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

Equations

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

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

Equations

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

def Lean.MacroScopesView.equalScope (a : Lean.MacroScopesView) (b : Lean.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 : 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

@[reducible, 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} [Monad m] [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.
• 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] [Lean.MonadEnv m] [Lean.MonadError m] (k : Lake.Name) : m Lake.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] [Lean.MonadEnv m] [Lean.MonadError m] (k : Lake.Name) : Lake.Name → m Lake.Name

Equations

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

Equations

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

def Lean.Elab.syntaxNodeKindOfAttrParam (defaultParserNamespace : Lake.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 : 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.

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.instMonadMacroAdapterOfMonadLift (m : Type → Type) (n : Type → Type) [MonadLift m n] [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} [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 α

Equations

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

@[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

Equations

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

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

Equations

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

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

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] [Lean.MonadLog m] [MonadExcept Lean.Exception m] [Lean.AddMessageContext m] [Lean.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] [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} [Lean.MonadError m] [Monad m] [Lean.MonadLog m] (msg : Lean.MessageData) (exs : Array Lean.Exception) : m α

Equations

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