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

Equations

• stx.prettyPrint = match stx.unsetTrailing.reprint with | some str => Std.format str.toFormat | none => Std.format stx

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

Equations

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

def Lean.MacroScopesView.equalScope (a b : MacroScopesView) : Bool

Two names are from the same lexical scope if their scoping information modulo MacroScopesView.name is equal.

Equations

• a.equalScope b = (a.scopes == b.scopes && a.mainModule == b.mainModule && a.imported == b.imported)

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

Equations

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

structure Lean.Elab.MacroStackElem : Type

• before : Syntax
• after : Syntax

@[reducible, inline]

abbrev Lean.Elab.MacroStack : Type

Equations

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

def Lean.Elab.getBetterRef (ref : Syntax) (macroStack : MacroStack) : 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} [Monad m] [MonadOptions m] (msgData : MessageData) (macroStack : MacroStack) : m MessageData

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.addMacroStack msgData [] = do let __do_lift ← Lean.getOptions if (!Lean.Option.get __do_lift Lean.Elab.pp.macroStack) = true then pure msgData else pure msgData

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

Equations

• Lean.Elab.checkSyntaxNodeKindAtNamespaces k (p.str str) = (Lean.Elab.checkSyntaxNodeKind (p.str str ++ k) <|> Lean.Elab.checkSyntaxNodeKindAtNamespaces k p)
• 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 : Name) : AttrM Name

Equations

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

def Lean.Elab.syntaxNodeKindOfAttrParam (defaultParserNamespace : Name) (stx : Syntax) : AttrM 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 : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax

unsafe def Lean.Elab.mkElabAttribute (γ : Type) (attrBuiltinName attrName parserNamespace typeName : Name) (kind : String) (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute γ)

Equations

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

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

Equations

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

@[implemented_by Lean.Elab.mkMacroAttributeUnsafe]

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

opaque Lean.Elab.macroAttribute : KeyedDeclsAttribute Macro

Registers a macro expander for a given syntax node kind.

A macro expander should have type Lean.Macro (which is Lean.Syntax → Lean.MacroM Lean.Syntax), i.e. should take syntax of the given syntax node kind as a parameter and produce different syntax in the same syntax category.

The macro_rules and macro commands should usually be preferred over using this attribute directly.

def Lean.Elab.expandMacroImpl? (env : Environment) : Syntax → MacroM (Option (Name × Except Macro.Exception 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 MacroScope
• getNextMacroScope : m MacroScope
• setNextMacroScope : MacroScope → m Unit

@[always_inline]

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.logException (Lean.Exception.error ref msg) = Lean.logErrorAt ref msg

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

If x throws an exception, catch it and turn it into a log message (using logException).

Equations

• Lean.Elab.withLogging x = tryCatch x fun (ex : Lean.Exception) => Lean.Elab.logException ex

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

Equations

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

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

Equations

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