- ref : Lean.Syntax
- modifiers : Lean.Elab.Modifiers
- kind : Lean.Elab.DefKind
Stores whether this is the header of a definition, theorem, ...
- shortDeclName : Lake.Name
- declName : Lake.Name
Full name for this declaration. This is the name that will be added to the
Universe level parameter names explicitly provided by the user.
Syntax objects for the binders occurring befor
:, we use them to populate the
- 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
Syntaxobject the body/value of the definition.
DefView after elaborating the header.
The let-recs may invoke each other. Example:
y is free variable in
z is a free variable in
z must be in the closure of both.
That is, we need to generate the top-level definitions.
sectionVars: The section variables used in the
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 definitions
letRecsToLift: The let-rec's definitions that need to be lifted