Instances For
If ref
does not have position information, then try to use macroStack
Instances For
def
Lean.Elab.addMacroStack
{m : Type → Type}
[Monad m]
[Lean.MonadOptions m]
(msgData : Lean.MessageData)
(macroStack : Lean.Elab.MacroStack)
:
Instances For
def
Lean.Elab.checkSyntaxNodeKind
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(k : Lake.Name)
:
Instances For
def
Lean.Elab.checkSyntaxNodeKindAtNamespaces
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(k : Lake.Name)
:
Equations
- One or more equations did not get rendered due to their size.
- Lean.Elab.checkSyntaxNodeKindAtNamespaces k Lean.Name.anonymous = Lean.Elab.checkSyntaxNodeKind k
- Lean.Elab.checkSyntaxNodeKindAtNamespaces k x = Lean.throwError (Lean.toMessageData "failed")
Instances For
Instances For
Instances For
@[implemented_by _private.Lean.Elab.Util.0.Lean.Elab.evalSyntaxConstantUnsafe]
opaque
Lean.Elab.evalSyntaxConstant
(env : Lean.Environment)
(opts : Lean.Options)
(constName : Lake.Name)
:
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
.
Instances For
- getCurrMacroScope : m Lean.MacroScope
- getNextMacroScope : m Lean.MacroScope
- setNextMacroScope : Lean.MacroScope → m Unit
Instances
@[always_inline]
instance
Lean.Elab.instMonadMacroAdapter
(m : Type → Type)
(n : Type → Type)
[MonadLift m n]
[Lean.Elab.MonadMacroAdapter m]
:
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 α
Instances For
@[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)
:
Instances For
partial def
Lean.Elab.mkUnusedBaseName.loop
(baseName : Lake.Name)
(currNamespace : Lake.Name)
(idx : Nat)
:
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
Instances For
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
Instances For
def
Lean.Elab.nestedExceptionToMessageData
{m : Type → Type}
[Monad m]
[Lean.MonadLog m]
(ex : Lean.Exception)
:
Instances For
def
Lean.Elab.throwErrorWithNestedErrors
{m : Type → Type}
{α : Type}
[Lean.MonadError m]
[Monad m]
[Lean.MonadLog m]
(msg : Lean.MessageData)
(exs : Array Lean.Exception)
:
m α