structure Lean.Elab.Command.State : Type

• env : Environment
• messages : MessageLog
• scopes : List Scope
• usedQuotCtxts : NameSet
• nextMacroScope : Nat
• maxRecDepth : Nat
• ngen : NameGenerator
• auxDeclNGen : DeclNameGenerator
• infoState : InfoState
• traceState : TraceState
• snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree)

instance Lean.Elab.Command.instNonemptyState : Nonempty State

structure Lean.Elab.Command.Context : Type

• fileName : String
• fileMap : FileMap
• currRecDepth : Nat
• cmdPos : String.Pos.Raw
• macroStack : MacroStack
• quotContext? : Option Name
• currMacroScope : MacroScope
• ref : Syntax
• snap? : Option (Language.SnapshotBundle Language.DynamicSnapshot)

  Snapshot for incremental reuse and reporting of command elaboration. Currently only used for (mutual) defs and contained tactics, in which case the DynamicSnapshot is a HeadersParsedSnapshot.

  Definitely resolved in Lean.Elab.Command.elabCommandTopLevel.

  Invariant: if the bundle's old? is set, the context and state at the beginning of current and old elaboration are identical.

• cancelTk? : Option IO.CancelToken

  Cancellation token forwarded to Core.cancelTk?.

• suppressElabErrors : Bool

  If set (when showPartialSyntaxErrors is not set and parsing failed), suppresses most elaboration errors; see also logMessage below.

@[reducible, inline]

abbrev Lean.Elab.Command.CommandElabM (α : Type) : Type

@[reducible, inline]

abbrev Lean.Elab.Command.CommandElab : Type

structure Lean.Elab.Command.Linter : Type

• run : Syntax → CommandElabM Unit
• name : Name

@[implicit_reducible, always_inline]

instance Lean.Elab.Command.instMonadCommandElabM : Monad CommandElabM

@[inline]

def Lean.Elab.Command.tryCatch {α : Type} (x : CommandElabM α) (h : Exception → CommandElabM α) : CommandElabM α

Like Core.tryCatchRuntimeEx; runtime errors are generally used to abort term elaboration, so we do want to catch and process them at the command level.

@[implicit_reducible]

instance Lean.Elab.Command.instMonadExceptOfExceptionCommandElabM : MonadExceptOf Exception CommandElabM

def Lean.Elab.Command.mkState (env : Environment) (messages : MessageLog := { }) (opts : Options := ∅) : State

opaque Lean.Elab.Command.lintersRef : IO.Ref (Array Linter)

def Lean.Elab.Command.addLinter (l : Linter) : IO Unit

@[implicit_reducible]

instance Lean.Elab.Command.instMonadInfoTreeCommandElabM : MonadInfoTree CommandElabM

@[implicit_reducible]

instance Lean.Elab.Command.instMonadEnvCommandElabM : MonadEnv CommandElabM

@[implicit_reducible, always_inline]

instance Lean.Elab.Command.instMonadOptionsCommandElabM : MonadOptions CommandElabM

def Lean.Elab.Command.getRef : CommandElabM Syntax

@[implicit_reducible]

instance Lean.Elab.Command.instAddMessageContextCommandElabM : AddMessageContext CommandElabM

@[implicit_reducible]

instance Lean.Elab.Command.instMonadRefCommandElabM : MonadRef CommandElabM

@[implicit_reducible]

instance Lean.Elab.Command.instMonadTraceCommandElabM : MonadTrace CommandElabM

@[implicit_reducible]

instance Lean.Elab.Command.instAddErrorMessageContextCommandElabM : AddErrorMessageContext CommandElabM

@[implicit_reducible]

instance Lean.Elab.Command.instMonadDeclNameGeneratorCommandElabM : MonadDeclNameGenerator CommandElabM

def Lean.Elab.Command.getCurrMacroScope : CommandElabM Nat

def Lean.Elab.Command.getMainModule : CommandElabM Name

def Lean.Elab.Command.withFreshMacroScope {α : Type} (x : CommandElabM α) : CommandElabM α

@[implicit_reducible]

instance Lean.Elab.Command.instMonadQuotationCommandElabM : MonadQuotation CommandElabM

def Lean.Elab.Command.liftCoreM {α : Type} (x : CoreM α) : CommandElabM α

@[inline]

def Lean.Elab.Command.liftIO {α : Type} (x : IO α) : CommandElabM α

@[implicit_reducible]

instance Lean.Elab.Command.instMonadLiftTIOCommandElabM : MonadLiftT IO CommandElabM

def Lean.Elab.Command.getScope : CommandElabM Scope

Return the current scope.

@[implicit_reducible]

instance Lean.Elab.Command.instMonadResolveNameCommandElabM : MonadResolveName CommandElabM

@[implicit_reducible]

instance Lean.Elab.Command.instMonadLogCommandElabM : MonadLog CommandElabM

def Lean.Elab.Command.runLinters (stx : Syntax) : CommandElabM Unit

@[inline]

def Lean.Elab.Command.withLoggingExceptions (x : CommandElabM Unit) : CommandElabM Unit

Catches and logs exceptions occurring in x. Unlike try catch in CommandElabM, this function catches interrupt exceptions as well and thus is intended for use at the top level of elaboration. Interrupt and abort exceptions are caught but not logged.

def Lean.Elab.Command.wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option IO.CancelToken) : CommandElabM (α → EIO Exception β)

Wraps the given action for use in EIO.asTask etc., discarding its final monadic state.

def Lean.Elab.Command.wrapAsyncAsSnapshot {α : Type} (act : α → CommandElabM Unit) (cancelTk? : Option IO.CancelToken) (desc : String := by exact decl_name%.toString) : CommandElabM (α → BaseIO Language.SnapshotTree)

Wraps the given action for use in BaseIO.asTask etc., discarding its final state except for logSnapshotTask tasks, which are reported as part of the returned tree. The given cancellation token, if any, should be stored in a SnapshotTask for the server to trigger it when the result is no longer needed.

def Lean.Elab.Command.logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CommandElabM Unit

Includes a given task (such as from wrapAsyncAsSnapshot) in the overall snapshot tree for this command's elaboration, making its result available to reporting and the language server. The reporter will not know about this snapshot tree node until the main elaboration thread for this command has finished so this function is not useful for incremental reporting within a longer elaboration thread but only for tasks that outlive it such as background kernel checking or proof elaboration.

def Lean.Elab.Command.runLintersAsync (stx : Syntax) : CommandElabM Unit

opaque Lean.Elab.Command.commandElabAttribute : KeyedDeclsAttribute CommandElab

Registers a command elaborator for the given syntax node kind.

A command elaborator should have type Lean.Elab.Command.CommandElab (which is Lean.Syntax → Lean.Elab.Term.CommandElabM Unit), i.e. should take syntax of the given syntax node kind as a parameter and perform an action.

The elab_rules and elab commands should usually be preferred over using this attribute directly.

def Lean.Elab.Command.withoutCommandIncrementality {α : Type} (cond : Bool) (act : CommandElabM α) : CommandElabM α

Disables incremental command reuse and reporting for act if cond is true by setting Context.snap? to none.

def Lean.Elab.Command.withMacroExpansion {α : Type} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α

Elaborate x with stx on the macro stack

@[implicit_reducible]

instance Lean.Elab.Command.instMonadMacroAdapterCommandElabM : MonadMacroAdapter CommandElabM

@[implicit_reducible]

instance Lean.Elab.Command.instMonadRecDepthCommandElabM : MonadRecDepth CommandElabM

structure Lean.Elab.Command.MacroExpandedSnapshotextends Lean.Language.Snapshot : Type

Snapshot after macro expansion of a command.

• desc : String
• diagnostics : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• macroDecl : Name

  The declaration name of the macro.

• newStx : Syntax

  The expanded syntax tree.

• newNextMacroScope : Nat

  State.nextMacroScope after expansion.

• hasTraces : Bool

  Whether any traces were present after expansion.

• next : Array (Language.SnapshotTask Language.DynamicSnapshot)

  Follow-up elaboration snapshots, one per command if newStx is a sequence of commands.

@[implicit_reducible]

instance Lean.Elab.Command.instTypeNameMacroExpandedSnapshot : TypeName MacroExpandedSnapshot

@[implicit_reducible]

instance Lean.Elab.Command.instToSnapshotTreeMacroExpandedSnapshot : Language.ToSnapshotTree MacroExpandedSnapshot

partial def Lean.Elab.Command.elabCommand (stx : Syntax) : CommandElabM Unit

opaque Lean.Elab.Command.showPartialSyntaxErrors : Lean.Option Bool

Option for showing elaboration errors from partial syntax errors.

def Lean.Elab.Command.withInitQuotContext (hint? : Option UInt64) (act : CommandElabM Unit) : CommandElabM Unit

If hint? is some hint, establishes a new context for macro scope naming and runs act in it, otherwise runs act directly without changes.

Context names as documented in Note Macro Scope Representation help with avoiding rebuilds and prefer_native lookup misses from macro scopes in declaration names and other exported information. This function establishes a new context with a globally unique name by combining the name of the current module with hint while also checking for previously used hints in the same module. Thus hint does not need to be unique but ensuring it is usually unique helps with keeping the context name stable.

In the current implementation, we call withInitQuotContext once in elabCommandTopLevel using the source input of the command as the hint. This helps with keeping macro scopes stable on changes to other parts of the file but not on changes to the command itself. Thus in each declaration elaborator we call withInitQuotContext again with the declaration name(s) as a hint so that changes to any other part of the declaration do not change the context name.

def Lean.Elab.Command.elabCommandTopLevel (stx : Syntax) : CommandElabM Unit

elabCommand wrapper that should be used for the initial invocation, not for recursive calls after macro expansion etc.

def Lean.Elab.Command.adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab

Adapt a syntax transformation to a regular, command-producing elaborator.

@[implicit_reducible]

instance Lean.Elab.Command.instInhabitedCommandElabM {α : Type} : Inhabited (CommandElabM α)

def Lean.Elab.Command.mkMetaContext : Meta.Context

The environment linter framework needs to be able to run linters with the same context as liftTermElabM, so we expose that context as a public function here.

def Lean.Elab.Command.getBracketedBinderIds : Syntax → CommandElabM (Array Name)

Return identifier names in the given bracketed binder.

def Lean.Elab.Command.liftTermElabM {α : Type} (x : TermElabM α) : CommandElabM α

Lift the TermElabM monadic action x into a CommandElabM monadic action.

Note that x is executed with an empty message log. Thus, x cannot modify/view messages produced by previous commands.

If you need to access the free variables corresponding to the ones declared using the variable command, consider using runTermElabM.

Recall that TermElabM actions can automatically lift MetaM and CoreM actions. Example:

public import Lean

open Lean Elab Command Meta

def printExpr (e : Expr) : MetaM Unit := do
  IO.println s!"{← ppExpr e} : {← ppExpr (← inferType e)}"

#eval
  liftTermElabM do
    printExpr (mkConst ``Nat)

@[implicit_reducible]

instance Lean.Elab.Command.instMonadEvalTermElabMCommandElabM : MonadEval TermElabM CommandElabM

def Lean.Elab.Command.runTermElabM {α : Type} (elabFn : Array Expr → TermElabM α) : CommandElabM α

Execute the monadic action elabFn xs as a CommandElabM monadic action, where xs are free variables corresponding to all active scoped variables declared using the variable command.

This method is similar to liftTermElabM, but it elaborates all scoped variables declared using the variable command.

Example:

public import Lean

public section

open Lean Elab Command Meta

variable {α : Type u} {f : α → α}
variable (n : Nat)

#eval
  runTermElabM fun xs => do
    for x in xs do
      IO.println s!"{← ppExpr x} : {← ppExpr (← inferType x)}"

def Lean.Elab.Command.getScopes : CommandElabM (List Scope)

Return the stack of all currently active scopes: the base scope always comes last; new scopes are prepended in the front. In particular, the current scope is always the first element.

def Lean.Elab.Command.modifyScope (f : Scope → Scope) : CommandElabM Unit

def Lean.Elab.Command.withScope {α : Type} (f : Scope → Scope) (x : CommandElabM α) : CommandElabM α

def Lean.Elab.Command.getLevelNames : CommandElabM (List Name)

def Lean.Elab.Command.addUnivLevel (idStx : Syntax) : CommandElabM Unit

def Lean.liftCommandElabM {α : Type} (cmd : Elab.Command.CommandElabM α) (throwOnError : Bool := true) : CoreM α

Lifts an action in CommandElabM into CoreM, updating the environment, messages, info trees, traces, the name generator, and macro scopes. The action is run in a context with an empty message log, empty trace state, and empty info trees.

If throwOnError is true, then if the command produces an error message, it is converted into an exception. In this case, info trees and messages are not carried over.

Commands that modify the processing of subsequent commands, such as open and namespace commands, only have an effect for the remainder of the CommandElabM computation passed here, and do not affect subsequent commands.

Warning: when using this from MetaM monads, the caches are not reset. If the command defines new instances for example, you should use Lean.Meta.resetSynthInstanceCache to reset the instance cache. While the modifyEnv function for MetaM clears its caches entirely, liftCommandElabM has no way to reset these caches.

partial def Lean.withSetOptionIn (cmd : Elab.Command.CommandElab) : Elab.Command.CommandElab

Given a command elaborator cmd, returns a new command elaborator that first evaluates any local set_option ... in ... clauses and then invokes cmd on what remains.