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

Equations

• Lean.Syntax.prettyPrint stx = match Lean.Syntax.reprint (Lean.Syntax.unsetTrailing stx) with | some str => Std.format (String.toFormat str) | none => Std.format stx

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.MacroStackElem : Type

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

@[inline]

abbrev Lean.Elab.MacroStack : Type

Equations

• Lean.Elab.MacroStack = List Lean.Elab.MacroStackElem

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.checkSyntaxNodeKind k = do let __do_lift ← Lean.getEnv if Lean.Parser.isValidSyntaxNodeKind __do_lift k = true then pure k else Lean.throwError (Lean.toMessageData "failed")

def Lean.Elab.checkSyntaxNodeKindAtNamespaces {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (k : Lean.Name) : Lean.Name → m Lean.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 : Lean.Name) : Lean.AttrM Lean.Name

Equations

• Lean.Elab.checkSyntaxNodeKindAtCurrentNamespaces k = do let ctx ← read Lean.Elab.checkSyntaxNodeKindAtNamespaces k ctx.currNamespace

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.mkMacroAttributeUnsafe ref = Lean.Elab.mkElabAttribute Lean.Macro `builtin_macro `macro Lean.Name.anonymous `Lean.Macro "macro"

@[implemented_by Lean.Elab.mkMacroAttributeUnsafe]

opaque Lean.Elab.mkMacroAttribute (ref : Lean.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 (Lean.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.

Equations

• One or more equations did not get rendered due to their size.

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) [inst : MonadLift m n] [inst : Lean.Elab.MonadMacroAdapter m] : Lean.Elab.MonadMacroAdapter n

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• Lean.Elab.adaptMacro x stx = Lean.Elab.liftMacroM (x stx)

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.withLogging x = tryCatch x fun ex => Lean.Elab.logException ex

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.