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 : Lean.Name) : Lean.Format

Equations

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

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

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

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

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

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 : Lean.Name) : m Lean.Name

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

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 attrName parserNamespace typeName : Lean.Name) (kind : String) (attrDeclName : Lean.Name := by exact decl_name%) : IO (Lean.KeyedDeclsAttribute γ)

unsafe def Lean.Elab.mkMacroAttributeUnsafe (ref : Lean.Name) : IO (Lean.KeyedDeclsAttribute Lean.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.

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

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 currNamespace : Lean.Name) (idx : Nat) : Lean.MacroM Lean.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).

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 α

Equations

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