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