structure Lean.Elab.DefViewElabHeader : Type

• 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 at valueStx, 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.

• levelNames : List Lake.Name

  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 the InfoTree when elaborating valueStx.

• 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.

instance Lean.Elab.instInhabitedDefViewElabHeader : Inhabited Lean.Elab.DefViewElabHeader

Equations

• One or more equations did not get rendered due to their size.

@[inline, reducible]

abbrev Lean.Elab.Term.MutualClosure.UsedFVarsMap : Type

A mapping from FVarId to Set of FVarIds.

Equations

• Lean.Elab.Term.MutualClosure.UsedFVarsMap = Lean.FVarIdMap Lean.FVarIdSet

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

structure Lean.Elab.Term.MutualClosure.FixPoint.State : Type

• usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap
• modified : Bool

@[inline, reducible]

abbrev Lean.Elab.Term.MutualClosure.FixPoint.M (α : Type) : Type

Equations

• Lean.Elab.Term.MutualClosure.FixPoint.M = ReaderT (Array Lean.FVarId) (StateM Lean.Elab.Term.MutualClosure.FixPoint.State)

def Lean.Elab.Term.MutualClosure.FixPoint.run (letRecFVarIds : Array Lean.FVarId) (usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap) : Lean.Elab.Term.MutualClosure.UsedFVarsMap

Equations

• One or more equations did not get rendered due to their size.

@[inline, reducible]

abbrev Lean.Elab.Term.MutualClosure.FreeVarMap : Type

Equations

• Lean.Elab.Term.MutualClosure.FreeVarMap = Lean.FVarIdMap (Array Lean.FVarId)

structure Lean.Elab.Term.MutualClosure.ClosureState : Type

• newLocalDecls : Array Lean.LocalDecl
• localDecls : Array Lean.LocalDecl
• newLetDecls : Array Lean.LocalDecl
• exprArgs : Array Lean.Expr

structure Lean.Elab.Term.MutualClosure.LetRecClosure : Type

• 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

@[inline, reducible]

abbrev Lean.Elab.Term.MutualClosure.Replacement : Type

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

Equations

• Lean.Elab.Term.MutualClosure.Replacement = Lean.FVarIdMap Lean.Expr

def Lean.Elab.Term.MutualClosure.insertReplacementForMainFns (r : Lean.Elab.Term.MutualClosure.Replacement) (sectionVars : Array Lean.Expr) (mainHeaders : Array Lean.Elab.DefViewElabHeader) (mainFVars : Array Lean.Expr) : Lean.Elab.Term.MutualClosure.Replacement

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.MutualClosure.insertReplacementForLetRecs (r : Lean.Elab.Term.MutualClosure.Replacement) (letRecClosures : List Lean.Elab.Term.MutualClosure.LetRecClosure) : Lean.Elab.Term.MutualClosure.Replacement

Equations

• Lean.Elab.Term.MutualClosure.insertReplacementForLetRecs r letRecClosures = List.foldl (fun r c => Lean.FVarIdMap.insert r c.toLift.fvarId c.closed) r letRecClosures

def Lean.Elab.Term.MutualClosure.Replacement.apply (r : Lean.Elab.Term.MutualClosure.Replacement) (e : Lean.Expr) : Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.MutualClosure.pushMain (preDefs : Array Lean.Elab.PreDefinition) (sectionVars : Array Lean.Expr) (mainHeaders : Array Lean.Elab.DefViewElabHeader) (mainVals : Array Lean.Expr) : Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.MutualClosure.pushLetRecs (preDefs : Array Lean.Elab.PreDefinition) (letRecClosures : List Lean.Elab.Term.MutualClosure.LetRecClosure) (kind : Lean.Elab.DefKind) (modifiers : Lean.Elab.Modifiers) : Lean.MetaM (Array Lean.Elab.PreDefinition)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.MutualClosure.getKindForLetRecs (mainHeaders : Array Lean.Elab.DefViewElabHeader) : Lean.Elab.DefKind

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.MutualClosure.getModifiersForLetRecs (mainHeaders : Array Lean.Elab.DefViewElabHeader) : Lean.Elab.Modifiers

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.MutualClosure.main (sectionVars : Array Lean.Expr) (mainHeaders : Array Lean.Elab.DefViewElabHeader) (mainFVars : Array Lean.Expr) (mainVals : Array Lean.Expr) (letRecsToLift : List Lean.Elab.Term.LetRecToLift) : Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)

• 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 : List Lake.Name) (preDefs : Array Lean.Elab.PreDefinition) : Lean.Elab.TermElabM Unit

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Elab.Term.checkForHiddenUnivLevels.visitLevel (allUserLevelNames : List Lake.Name) (sTypes : Lean.CollectLevelParams.State) (preDef : Lean.Elab.PreDefinition) (u : Lean.Level) : ReaderT Lean.Expr Lean.Elab.TermElabM Unit

partial def Lean.Elab.Term.checkForHiddenUnivLevels.visit (allUserLevelNames : List Lake.Name) (sTypes : Lean.CollectLevelParams.State) (preDef : Lean.Elab.PreDefinition) (e : Lean.Expr) : ReaderT Lean.Expr (Lean.MonadCacheT Lean.ExprStructEq Unit Lean.Elab.TermElabM) Unit

def Lean.Elab.Term.elabMutualDef (vars : Array Lean.Expr) (views : Array Lean.Elab.DefView) (hints : Lean.Elab.TerminationHints) : Lean.Elab.TermElabM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabMutualDef.go (vars : Array Lean.Expr) (views : Array Lean.Elab.DefView) (hints : Lean.Elab.TerminationHints) : Lean.Elab.TermElabM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.elabMutualDef.processDeriving (views : Array Lean.Elab.DefView) (headers : Array Lean.Elab.DefViewElabHeader) : Lean.Elab.TermElabM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.elabMutualDef (ds : Array Lean.Syntax) (hints : Lean.Elab.TerminationHints) : Lean.Elab.Command.CommandElabM Unit

Equations

• One or more equations did not get rendered due to their size.