Equations
Instances For
Two names are from the same lexical scope if their scoping information modulo MacroScopesView.name
is equal.
Equations
Instances For
If ref
does not have position information, then try to use macroStack
Equations
Instances For
def
Lean.Elab.addMacroStack
{m : Type → Type}
[Monad m]
[MonadOptions m]
(msgData : MessageData)
(macroStack : MacroStack)
:
Equations
Instances For
def
Lean.Elab.checkSyntaxNodeKind
{m : Type → Type}
[Monad m]
[MonadEnv m]
[MonadError m]
(k : Name)
:
m Name
Equations
Instances For
def
Lean.Elab.checkSyntaxNodeKindAtNamespaces
{m : Type → Type}
[Monad m]
[MonadEnv m]
[MonadError m]
(k : Name)
:
Equations
Instances For
Equations
Instances For
Equations
Instances For
@[implemented_by _private.Lean.Elab.Util.0.Lean.Elab.evalSyntaxConstantUnsafe]
unsafe def
Lean.Elab.mkElabAttribute
(γ : Type)
(attrBuiltinName attrName parserNamespace typeName : Name)
(kind : String)
(attrDeclName : Name := by exact decl_name%)
:
Equations
Instances For
Equations
Instances For
@[implemented_by Lean.Elab.mkMacroAttributeUnsafe]
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
Instances For
- getCurrMacroScope : m MacroScope
- getNextMacroScope : m MacroScope
- setNextMacroScope : MacroScope → m Unit
Instances
@[always_inline]
instance
Lean.Elab.instMonadMacroAdapterOfMonadLift
(m n : Type → Type)
[MonadLift m n]
[MonadMacroAdapter m]
:
Equations
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
Instances For
@[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
Instances For
def
Lean.Elab.logException
{m : Type → Type}
[Monad m]
[MonadLog m]
[AddMessageContext m]
[MonadOptions m]
[MonadLiftT IO m]
(ex : Exception)
:
m Unit
Equations
Instances For
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
Instances For
def
Lean.Elab.throwErrorWithNestedErrors
{m : Type → Type}
{α : Type}
[MonadError m]
[Monad m]
[MonadLog m]
(msg : MessageData)
(exs : Array Exception)
:
m α