structure Lean.Elab.Command.Scope : Type

• header : String
• opts : Lean.Options
• currNamespace : Lake.Name
• openDecls : List Lean.OpenDecl
• levelNames : List Lake.Name
• varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)

  section variables

• varUIds : Array Lake.Name

  Globally unique internal identifiers for the varDecls

• isNoncomputable : Bool

  noncomputable sections automatically add the noncomputable modifier to any declaration we cannot generate code for.

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
• nextInstIdx : 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 = Lean.Elab.Command.instNonemptyState.proof_1

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)

@[inline, reducible]

abbrev Lean.Elab.Command.CommandElabCoreM (ε : Type) (α : Type) : Type

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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 : Lake.Name

@[always_inline]

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

Equations

• Lean.Elab.Command.instMonadCommandElabM = let i := inferInstanceAs (Monad Lean.Elab.Command.CommandElabM); Monad.mk

def Lean.Elab.Command.mkState (env : Lean.Environment) (messages : optParam Lean.MessageLog { msgs := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) (opts : optParam 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 (Array.push ls 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 (List.head! __do_lift.scopes).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

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

@[inline]

def Lean.Elab.Command.liftEIO {α : Type} (x : EIO Lean.Exception α) : Lean.Elab.Command.CommandElabM α

Equations

• Lean.Elab.Command.liftEIO x = liftM x

@[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 => Lean.Exception.error ctx.ref ((Lean.MessageData.ofFormat ∘ Std.format) (IO.Error.toString ex))) x)

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

Equations

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

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

Equations

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

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 Lake.Name

Equations

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

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

• Lean.Elab.Command.instMonadQuotationCommandElabM = Lean.MonadQuotation.mk Lean.Elab.Command.getCurrMacroScope Lean.Elab.Command.getMainModule fun {α} => Lean.Elab.Command.withFreshMacroScope

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

Equations

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

@[implemented_by Lean.Elab.Command.mkCommandElabAttributeUnsafe]

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

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

def Lean.Elab.Command.withMacroExpansion {α : Type} (beforeStx : Lean.Syntax) (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.

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

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

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 → Array Lake.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.

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

Equations

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

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

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 Lake.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.Elab.Command.expandDeclId (declId : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) : Lean.Elab.Command.CommandElabM Lean.Elab.ExpandDeclIdResult

Equations

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