def Lean.Syntax.prettyPrint (stx : Lean.Syntax) : Lean.Format

def Lean.MacroScopesView.format (view : Lean.MacroScopesView) (mainModule : Lake.Name) : Lean.Format

def Lean.Elab.expandOptNamedPrio (stx : Lean.Syntax) : Lean.MacroM Nat

structure Lean.Elab.MacroStackElem : Type

• before : Lean.Syntax
• after : Lean.Syntax

@[inline, reducible]

abbrev Lean.Elab.MacroStack : Type

def Lean.Elab.getBetterRef (ref : Lean.Syntax) (macroStack : Lean.Elab.MacroStack) : Lean.Syntax

If ref does not have position information, then try to use macroStack

opaque Lean.Elab.pp.macroStack : Lean.Option Bool

def Lean.Elab.addMacroStack {m : Type → Type} [Monad m] [Lean.MonadOptions m] (msgData : Lean.MessageData) (macroStack : Lean.Elab.MacroStack) : m Lean.MessageData

def Lean.Elab.checkSyntaxNodeKind {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (k : Lake.Name) : m Lake.Name

def Lean.Elab.checkSyntaxNodeKindAtNamespaces {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (k : Lake.Name) : Lake.Name → m Lake.Name

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.checkSyntaxNodeKindAtNamespaces k Lean.Name.anonymous = Lean.Elab.checkSyntaxNodeKind k
• Lean.Elab.checkSyntaxNodeKindAtNamespaces k x = Lean.throwError (Lean.toMessageData "failed")

def Lean.Elab.checkSyntaxNodeKindAtCurrentNamespaces (k : Lake.Name) : Lean.AttrM Lake.Name

def Lean.Elab.syntaxNodeKindOfAttrParam (defaultParserNamespace : Lake.Name) (stx : Lean.Syntax) : Lean.AttrM Lean.SyntaxNodeKind

@[implemented_by _private.Lean.Elab.Util.0.Lean.Elab.evalSyntaxConstantUnsafe]

opaque Lean.Elab.evalSyntaxConstant (env : Lean.Environment) (opts : Lean.Options) (constName : Lake.Name) : ExceptT String Id Lean.Syntax

unsafe def Lean.Elab.mkElabAttribute (γ : Type) (attrBuiltinName : Lake.Name) (attrName : Lake.Name) (parserNamespace : Lake.Name) (typeName : Lake.Name) (kind : String) (attrDeclName : autoParam Lake.Name _auto✝) : IO (Lean.KeyedDeclsAttribute γ)

unsafe def Lean.Elab.mkMacroAttributeUnsafe (ref : Lake.Name) : IO (Lean.KeyedDeclsAttribute Lean.Macro)

@[implemented_by Lean.Elab.mkMacroAttributeUnsafe]

opaque Lean.Elab.mkMacroAttribute (ref : Lake.Name) : IO (Lean.KeyedDeclsAttribute Lean.Macro)

opaque Lean.Elab.macroAttribute : Lean.KeyedDeclsAttribute Lean.Macro

def Lean.Elab.expandMacroImpl? (env : Lean.Environment) : Lean.Syntax → Lean.MacroM (Option (Lake.Name × Except Lean.Macro.Exception Lean.Syntax))

Try to expand macro at syntax tree root and return macro declaration name and new syntax if successful. Return none if all macros threw Macro.Exception.unsupportedSyntax.

class Lean.Elab.MonadMacroAdapter (m : Type → Type) : Type

• getCurrMacroScope : m Lean.MacroScope
• getNextMacroScope : m Lean.MacroScope
• setNextMacroScope : Lean.MacroScope → m Unit

@[always_inline]

instance Lean.Elab.instMonadMacroAdapter (m : Type → Type) (n : Type → Type) [MonadLift m n] [Lean.Elab.MonadMacroAdapter m] : Lean.Elab.MonadMacroAdapter n

def Lean.Elab.liftMacroM {m : Type → Type} {α : Type} [Monad m] [Lean.Elab.MonadMacroAdapter m] [Lean.MonadEnv m] [Lean.MonadRecDepth m] [Lean.MonadError m] [Lean.MonadResolveName m] [Lean.MonadTrace m] [Lean.MonadOptions m] [Lean.AddMessageContext m] [MonadLiftT IO m] (x : Lean.MacroM α) : m α

@[inline]

def Lean.Elab.adaptMacro {m : Type → Type} [Monad m] [Lean.Elab.MonadMacroAdapter m] [Lean.MonadEnv m] [Lean.MonadRecDepth m] [Lean.MonadError m] [Lean.MonadResolveName m] [Lean.MonadTrace m] [Lean.MonadOptions m] [Lean.AddMessageContext m] [MonadLiftT IO m] (x : Lean.Macro) (stx : Lean.Syntax) : m Lean.Syntax

def Lean.Elab.mkUnusedBaseName (baseName : Lake.Name) : Lean.MacroM Lake.Name

partial def Lean.Elab.mkUnusedBaseName.loop (baseName : Lake.Name) (currNamespace : Lake.Name) (idx : Nat) : Lean.MacroM Lake.Name

def Lean.Elab.logException {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [MonadLiftT IO m] (ex : Lean.Exception) : m Unit

def Lean.Elab.withLogging {m : Type → Type} [Monad m] [Lean.MonadLog m] [MonadExcept Lean.Exception m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [MonadLiftT IO m] (x : m Unit) : m Unit

def Lean.Elab.nestedExceptionToMessageData {m : Type → Type} [Monad m] [Lean.MonadLog m] (ex : Lean.Exception) : m Lean.MessageData

def Lean.Elab.throwErrorWithNestedErrors {m : Type → Type} {α : Type} [Lean.MonadError m] [Monad m] [Lean.MonadLog m] (msg : Lean.MessageData) (exs : Array Lean.Exception) : m α