Documentation

Lean.Elab.Util

source
def Lean.Syntax.prettyPrint (stx : Lean.Syntax) :
Lean.Format
Equations
source
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.
source
def Lean.Elab.expandOptNamedPrio (stx : Lean.Syntax) :
Lean.MacroM Nat
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Elab.MacroStackElem:
Type
source
@[inline]
abbrev Lean.Elab.MacroStack:
Type
Equations
source
def Lean.Elab.getBetterRef (ref : Lean.Syntax) (macroStack : Lean.Elab.MacroStack) :
Lean.Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
opaque Lean.Elab.pp.macroStack:
Lean.Option Bool
source
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.
source
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
source
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
source
def Lean.Elab.checkSyntaxNodeKindAtCurrentNamespaces (k : Lean.Name) :
Lean.AttrM Lean.Name
Equations
source
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.
source
@[implementedBy _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
source
unsafe def Lean.Elab.mkElabAttribute (γ : Type) (attrDeclName : Lean.Name) (attrBuiltinName : Lean.Name) (attrName : Lean.Name) (parserNamespace : Lean.Name) (typeName : Lean.Name) (kind : String) :
IO (Lean.KeyedDeclsAttribute γ)
Equations
  • One or more equations did not get rendered due to their size.
source
unsafe def Lean.Elab.mkMacroAttributeUnsafe:
IO (Lean.KeyedDeclsAttribute Lean.Macro)
Equations
source
@[implementedBy Lean.Elab.mkMacroAttributeUnsafe]
opaque Lean.Elab.mkMacroAttribute:
IO (Lean.KeyedDeclsAttribute Lean.Macro)
source
opaque Lean.Elab.macroAttribute:
Lean.KeyedDeclsAttribute Lean.Macro
source
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.
source
class Lean.Elab.MonadMacroAdapter (m : Type → Type) :
Type
Instances
source
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.
source
def Lean.Elab.liftMacroM {α : Type} {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] (x : Lean.MacroM α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
@[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] (x : Lean.Macro) (stx : Lean.Syntax) :
m Lean.Syntax
Equations
source
def Lean.Elab.mkUnusedBaseName (baseName : Lean.Name) :
Lean.MacroM Lean.Name
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.mkUnusedBaseName.loop (baseName : Lean.Name) (currNamespace : Lean.Name) (idx : Nat) :
Lean.MacroM Lean.Name
source
def Lean.Elab.logException {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : MonadLiftT IO m] (ex : Lean.Exception) :
m Unit
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Elab.trace {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (cls : Lean.Name) (msg : Unit → Lean.MessageData) :
m Unit
Equations
source
def Lean.Elab.logDbgTrace {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (msg : Lean.MessageData) :
m Unit
Equations
source
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.
source
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.