# Documentation

Lean.Elab.Command

• currNamespace : Lean.Name
• openDecls :
• levelNames :
• section variables

varDecls : Array (Lean.TSyntax Lean.Parser.Term.bracketedBinder)
• Globally unique internal identifiers for the varDecls

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

isNoncomputable : Bool
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Instances For
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[always_inline]
Equations
def Lean.Elab.Command.mkState (env : Lean.Environment) (messages : optParam Lean.MessageLog { msgs := { root := , tail := , size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) (opts : optParam Lean.Options { entries := [] }) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• = do let ls ←
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[always_inline]
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Command.liftCoreM {α : Type} (x : ) :
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.Elab.Command.liftEIO {α : Type} (x : ) :
Equations
@[inline]
def Lean.Elab.Command.liftIO {α : Type} (x : IO α) :
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by Lean.Elab.Command.mkCommandElabAttributeUnsafe]
def Lean.Elab.Command.withMacroExpansion {α : Type} (beforeStx : Lean.Syntax) (afterStx : Lean.Syntax) :

Elaborate x with stx on the macro stack

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

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.

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

Equations
• = do let stx' ← exp stx
Equations
• Lean.Elab.Command.instInhabitedCommandElabM = { default := throw default }

Return identifier names in the given bracketed binder.

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

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)
← ppExpr e} : {← ppExpr (← inferType e)}"

#eval
liftTermElabM do
printExpr (mkConst Nat)
← ppExpr (← inferType e)}"

#eval
liftTermElabM do
printExpr (mkConst Nat)
← 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 : ) :

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)}"
→ α}
variable (n : Nat)

#eval
runTermElabM fun xs => do
for x in xs do
IO.println s!"{← ppExpr x} : {← ppExpr (← inferType x)}"
← ppExpr x} : {← ppExpr (← inferType x)}"
← ppExpr (← inferType x)}"
← inferType x)}"
`
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.