- header : String
- opts : Lean.Options
- currNamespace : Lake.Name
- openDecls : List Lean.OpenDecl
- varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)
section variables
Globally unique internal identifiers for the
varDecls
- isNoncomputable : Bool
noncomputable sections automatically add the
noncomputable
modifier to any declaration we cannot generate code for.
Instances For
- 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
Instances For
- 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)
Instances For
Instances For
- name : Lake.Name
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Elaborate x
with stx
on the macro stack
Instances For
elabCommand
wrapper that should be used for the initial invocation, not for recursive calls after
macro expansion etc.
Instances For
Adapt a syntax transformation to a regular, command-producing elaborator.
Instances For
Return identifier names in the given bracketed binder.
Instances For
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)
Instances For
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)}"