- ref : Lean.Syntax
- modifiers : Lean.Elab.Modifiers
- kind : Lean.Elab.DefKind
Stores whether this is the header of a definition, theorem, ...
- shortDeclName : Lake.Name
Short name. Recall that all declarations in Lean 4 are potentially recursive. We use
shortDeclName
to refer to them atvalueStx
, and other declarations in the same mutual block. - declName : Lake.Name
Full name for this declaration. This is the name that will be added to the
Environment
. Universe level parameter names explicitly provided by the user.
- binderIds : Array Lean.Syntax
Syntax objects for the binders occurring befor
:
, we use them to populate theInfoTree
when elaboratingvalueStx
. - numParams : Nat
Number of parameters before
:
, it also includes auto-implicit parameters automatically added by Lean. - type : Lean.Expr
Type including parameters.
- valueStx : Lean.Syntax
Syntax
object the body/value of the definition.
DefView
after elaborating the header.
Instances For
A mapping from FVarId to Set of FVarIds.
Instances For
The let-recs may invoke each other. Example:
let rec
f (x : Nat) := g x + y
g : Nat → Nat
| 0 => 1
| x+1 => f x + z
y
is free variable in f
, and z
is a free variable in g
.
To close f
and g
, y
and z
must be in the closure of both.
That is, we need to generate the top-level definitions.
def f (y z x : Nat) := g y z x + y
def g (y z : Nat) : Nat → Nat
| 0 => 1
| x+1 => f y z x + z
- usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap
- modified : Bool
Instances For
Instances For
Instances For
- newLocalDecls : Array Lean.LocalDecl
- localDecls : Array Lean.LocalDecl
- newLetDecls : Array Lean.LocalDecl
Instances For
- ref : Lean.Syntax
- localDecls : Array Lean.LocalDecl
- closed : Lean.Expr
Expression used to replace occurrences of the let-rec
FVarId
. - toLift : Lean.Elab.Term.LetRecToLift
Instances For
Mapping from FVarId of mutually recursive functions being defined to "closure" expression.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
sectionVars
: The section variables used in themutual
block.mainHeaders
: The elaborated header of the top-level definitions being defined by the mutual block.mainFVars
: The auxiliary variables used to represent the top-level definitions being defined by the mutual block.mainVals
: The elaborated value for the top-level definitionsletRecsToLift
: The let-rec's definitions that need to be lifted