structure Lean.Elab.Command.Scope : Type

A Scope records the part of the CommandElabM state that respects scoping, such as the data for universe, open, and variable declarations, the current namespace, and currently enabled options. The CommandElabM state contains a stack of scopes, and only the top Scope on the stack is read from or modified. There is always at least one Scope on the stack, even outside any section or namespace, and each new pushed Scope starts as a modified copy of the previous top scope.

• header : String

  The component of the namespace or section that this scope is associated to. For example, section a.b.c and namespace a.b.c each create three scopes with headers named a, b, and c. This is used for checking the end command. The "base scope" has "" as its header.

• opts : Lean.Options

  The current state of all set options at this point in the scope. Note that this is the full current set of options and does not simply contain the options set while this scope has been active.

• currNamespace : Lean.Name

  The current namespace. The top-level namespace is represented by Name.anonymous.

• openDecls : List Lean.OpenDecl

  All currently opened namespaces and names.

• levelNames : List Lean.Name

  The current list of names for universe level variables to use for new declarations. This is managed by the universe command.

• varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)

  The current list of binders to use for new declarations. This is managed by the variable command. Each binder is represented in Syntax form, and it is re-elaborated within each command that uses this information.

  This is also used by commands, such as #check, to create an initial local context, even if they do not work with binders per se.

• varUIds : Array Lean.Name

  Globally unique internal identifiers for the varDecls. There is one identifier per variable introduced by the binders (recall that a binder such as (a b c : Ty) can produce more than one variable), and each identifier is the user-provided variable name with a macro scope. This is used by TermElabM in Lean.Elab.Term.Context to help with processing macros that capture these variables.

• includedVars : List Lean.Name

  included section variable names (from varUIds)

• omittedVars : List Lean.Name

  omitted section variable names (from varUIds)

• isNoncomputable : Bool

  If true (default: false), all declarations that fail to compile automatically receive the noncomputable modifier. A scope with this flag set is created by noncomputable section.

  Recall that a new scope inherits all values from its parent scope, so all sections and namespaces nested within a noncomputable section also have this flag set.

instance Lean.Elab.Command.instInhabitedScope : Inhabited Lean.Elab.Command.Scope

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.Command.State : Type

• env : Lean.Environment
• messages : Lean.MessageLog
• scopes : List Lean.Elab.Command.Scope
• nextMacroScope : Nat
• maxRecDepth : Nat
• ngen : Lean.NameGenerator
• infoState : Lean.Elab.InfoState
• traceState : Lean.TraceState

instance Lean.Elab.Command.instNonemptyState : Nonempty Lean.Elab.Command.State

Equations

• Lean.Elab.Command.instNonemptyState = ⋯

structure Lean.Elab.Command.Context : Type

• fileName : String
• fileMap : Lean.FileMap
• currRecDepth : Nat
• cmdPos : String.Pos
• macroStack : Lean.Elab.MacroStack
• currMacroScope : Lean.MacroScope
• ref : Lean.Syntax
• tacticCache? : Option (IO.Ref Lean.Elab.Tactic.Cache)
• snap? : Option (Lean.Language.SnapshotBundle Lean.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 Language.Lean.process.doElab.

  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.CommandElabCoreM (ε α : Type) : Type

Equations

• Lean.Elab.Command.CommandElabCoreM ε = ReaderT Lean.Elab.Command.Context (StateRefT' IO.RealWorld Lean.Elab.Command.State (EIO ε))

@[reducible, inline]

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

Equations

• Lean.Elab.Command.CommandElabM = Lean.Elab.Command.CommandElabCoreM Lean.Exception

@[reducible, inline]

abbrev Lean.Elab.Command.CommandElab : Type

Equations

• Lean.Elab.Command.CommandElab = (Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)

structure Lean.Elab.Command.Linter : Type

• run : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
• name : Lean.Name

@[always_inline]

instance Lean.Elab.Command.instMonadCommandElabM : Monad Lean.Elab.Command.CommandElabM

Equations

• Lean.Elab.Command.instMonadCommandElabM = Monad.mk

@[inline]

def Lean.Elab.Command.tryCatch {α : Type} (x : Lean.Elab.Command.CommandElabM α) (h : Lean.Exception → Lean.Elab.Command.CommandElabM α) : Lean.Elab.Command.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.

Equations

• Lean.Elab.Command.tryCatch x h = tryCatch x fun (ex : Lean.Exception) => if ex.isInterrupt = true then throw ex else h ex

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

Equations

• Lean.Elab.Command.instMonadExceptOfExceptionCommandElabM = { throw := fun {α : Type} => throw, tryCatch := fun {α : Type} => Lean.Elab.Command.tryCatch }

def Lean.Elab.Command.mkState (env : Lean.Environment) (messages : Lean.MessageLog := { hadErrors := false, unreported := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, reportedKinds := ∅ }) (opts : Lean.Options := { entries := [] }) : Lean.Elab.Command.State

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.addLinter l = do let ls ← ST.Ref.get Lean.Elab.Command.lintersRef ST.Ref.set Lean.Elab.Command.lintersRef (ls.push l)

instance Lean.Elab.Command.instMonadInfoTreeCommandElabM : Lean.Elab.MonadInfoTree Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Elab.Command.instMonadEnvCommandElabM : Lean.MonadEnv Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

@[always_inline]

instance Lean.Elab.Command.instMonadOptionsCommandElabM : Lean.MonadOptions Lean.Elab.Command.CommandElabM

Equations

• Lean.Elab.Command.instMonadOptionsCommandElabM = { getOptions := do let __do_lift ← get pure __do_lift.scopes.head!.opts }

def Lean.Elab.Command.getRef : Lean.Elab.Command.CommandElabM Lean.Syntax

Equations

• Lean.Elab.Command.getRef = do let __do_lift ← read pure __do_lift.ref

instance Lean.Elab.Command.instAddMessageContextCommandElabM : Lean.AddMessageContext Lean.Elab.Command.CommandElabM

Equations

• Lean.Elab.Command.instAddMessageContextCommandElabM = { addMessageContext := Lean.addMessageContextPartial }

instance Lean.Elab.Command.instMonadRefCommandElabM : Lean.MonadRef Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Elab.Command.instMonadTraceCommandElabM : Lean.MonadTrace Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Elab.Command.instAddErrorMessageContextCommandElabM : Lean.AddErrorMessageContext Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.mkMessageAux (ctx : Lean.Elab.Command.Context) (ref : Lean.Syntax) (msgData : Lean.MessageData) (severity : Lean.MessageSeverity) : Lean.Message

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Command.liftCoreM x = do let __do_lift ← Lean.Elab.Command.runCore (observing x) ofExcept __do_lift

@[inline]

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

Equations

• Lean.Elab.Command.liftIO x = do let ctx ← read liftM (IO.toEIO (fun (ex : IO.Error) => Lean.Exception.error ctx.ref ((Lean.MessageData.ofFormat ∘ Lean.format) ex.toString)) x)

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

Equations

• Lean.Elab.Command.instMonadLiftTIOCommandElabM = { monadLift := fun {α : Type} => Lean.Elab.Command.liftIO }

def Lean.Elab.Command.getScope : Lean.Elab.Command.CommandElabM Lean.Elab.Command.Scope

Return the current scope.

Equations

• Lean.Elab.Command.getScope = do let __do_lift ← get pure __do_lift.scopes.head!

instance Lean.Elab.Command.instMonadResolveNameCommandElabM : Lean.MonadResolveName Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Elab.Command.instMonadLogCommandElabM : Lean.MonadLog Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.getCurrMacroScope : Lean.Elab.Command.CommandElabM Nat

Equations

• Lean.Elab.Command.getCurrMacroScope = do let __do_lift ← read pure __do_lift.currMacroScope

def Lean.Elab.Command.getMainModule : Lean.Elab.Command.CommandElabM Lean.Name

Equations

• Lean.Elab.Command.getMainModule = do let __do_lift ← Lean.getEnv pure __do_lift.mainModule

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Elab.Command.instMonadQuotationCommandElabM : Lean.MonadQuotation Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

unsafe def Lean.Elab.Command.mkCommandElabAttributeUnsafe (ref : Lean.Name) : IO (Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab)

@[implemented_by Lean.Elab.Command.mkCommandElabAttributeUnsafe]

opaque Lean.Elab.Command.mkCommandElabAttribute (ref : Lean.Name) : IO (Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab)

opaque Lean.Elab.Command.commandElabAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Elaborate x with stx on the macro stack

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Elab.Command.instMonadMacroAdapterCommandElabM : Lean.Elab.MonadMacroAdapter Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Elab.Command.instMonadRecDepthCommandElabM : Lean.MonadRecDepth Lean.Elab.Command.CommandElabM

Equations

• One or more equations did not get rendered due to their size.

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

Snapshot after macro expansion of a command.

• desc : String
• diagnostics : Lean.Language.Snapshot.Diagnostics
• infoTree? : Option Lean.Elab.InfoTree
• isFatal : Bool
• macroDecl : Lean.Name

  The declaration name of the macro.

• newStx : Lean.Syntax

  The expanded syntax tree.

• newNextMacroScope : Nat

  State.nextMacroScope after expansion.

• hasTraces : Bool

  Whether any traces were present after expansion.

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

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

instance Lean.Elab.Command.instTypeNameMacroExpandedSnapshot : TypeName Lean.Elab.Command.MacroExpandedSnapshot

Equations

• Lean.Elab.Command.instTypeNameMacroExpandedSnapshot = Lean.Elab.Command.inst✝

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Option for showing elaboration errors from partial syntax errors.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Elab.Command.adaptExpander exp stx = do let stx' ← exp stx Lean.Elab.Command.withMacroExpansion stx stx' (Lean.Elab.Command.elabCommand stx')

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

Equations

• Lean.Elab.Command.instInhabitedCommandElabM = { default := throw default }

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

Return identifier names in the given bracketed binder.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.liftTermElabM {α : Type} (x : Lean.Elab.TermElabM α) : Lean.Elab.Command.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:

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Command.instMonadEvalTermElabMCommandElabM = { monadEval := fun {α : Type} => Lean.Elab.Command.liftTermElabM }

def Lean.Elab.Command.runTermElabM {α : Type} (elabFn : Array Lean.Expr → Lean.Elab.TermElabM α) : Lean.Elab.Command.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:

import Lean

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)}"

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.Elab.Command.withLoggingExceptions (x : Lean.Elab.Command.CommandElabM Unit) : Lean.Elab.Command.CommandElabCoreM Empty 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.

Equations

• Lean.Elab.Command.withLoggingExceptions x ctx ref = (Lean.Elab.withLogging x ctx ref).catchExceptions fun (x : Lean.Exception) => pure ()

def Lean.Elab.Command.getScopes : Lean.Elab.Command.CommandElabM (List Lean.Elab.Command.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.

Equations

• Lean.Elab.Command.getScopes = do let __do_lift ← get pure __do_lift.scopes

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Command.getLevelNames = do let __do_lift ← Lean.Elab.Command.getScope pure __do_lift.levelNames

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.liftCommandElabM {α : Type} (cmd : Lean.Elab.Command.CommandElabM α) (throwOnError : Bool := true) : Lean.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.

Equations

• Lean.liftCommandElabM cmd throwOnError = do let __do_lift ← Lean.liftCommandElabMCore (observing cmd) throwOnError ofExcept __do_lift

partial def Lean.withSetOptionIn (cmd : Lean.Elab.Command.CommandElab) : Lean.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.