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

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

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.

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

structure Lean.Elab.MacroStackElem : Type

• before : Syntax
• after : Syntax

@[reducible, inline]

abbrev Lean.Elab.MacroStack : Type

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

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

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

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

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

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

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

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

class Lean.Elab.MonadMacroAdapter (m : Type → Type) extends Lean.MonadQuotation m : Type 1

• getRef : m Syntax
• withRef {α : Type} : Syntax → m α → m α
• getCurrMacroScope : m MacroScope
• getContext : m Name
• withFreshMacroScope {α : Type} : m α → m α
• getNextMacroScope : m MacroScope
• setNextMacroScope : MacroScope → m Unit

@[implicit_reducible, always_inline]

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

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 α

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

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

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

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

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

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