Documentation

Lean.Elab.MutualDef

• Stores whether this is the header of a definition, theorem, ...

• Short name. Recall that all declarations in Lean 4 are potentially recursive. We use shortDeclName to refer to them at valueStx, and other declarations in the same mutual block.

shortDeclName : Lean.Name
• Full name for this declaration. This is the name that will be added to the Environment.

declName : Lean.Name
• Universe level parameter names explicitly provided by the user.

levelNames :
• Syntax objects for the binders occurring befor :, we use them to populate the InfoTree when elaborating valueStx.

binderIds :
• Number of parameters before :, it also includes auto-implicit parameters automatically added by Lean.

numParams : Nat
• Type including parameters.

type : Lean.Expr
• Syntax object the body/value of the definition.

valueStx : Lean.Syntax

DefView after elaborating the header.

Instances For
Equations
• One or more equations did not get rendered due to their size.
@[inline]

A mapping from FVarId to Set of FVarIds.

Equations

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
→ 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
→ Nat
| 0 => 1
| x+1 => f y z x + z

Instances For
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
• newLocalDecls :
• localDecls :
• newLetDecls :
• exprArgs :
Instances For
Instances For
@[inline]

Mapping from FVarId of mutually recursive functions being defined to "closure" expression.

Equations
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.
def Lean.Elab.Term.MutualClosure.pushMain (preDefs : ) (sectionVars : ) (mainHeaders : ) (mainVals : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Term.MutualClosure.pushLetRecs (preDefs : ) (letRecClosures : ) (kind : Lean.Elab.DefKind) (modifiers : Lean.Elab.Modifiers) :
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.Term.MutualClosure.main (sectionVars : ) (mainHeaders : ) (mainFVars : ) (mainVals : ) (letRecsToLift : ) :
• sectionVars: The section variables used in the mutual 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 definitions
• letRecsToLift: The let-rec's definitions that need to be lifted
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Term.checkForHiddenUnivLevels (allUserLevelNames : ) (preDefs : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Term.elabMutualDef (vars : ) (views : ) (hints : Lean.Elab.TerminationHints) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Term.elabMutualDef.go (vars : ) (views : ) (hints : Lean.Elab.TerminationHints) :
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.