structure Lean.Elab.DefViewElabHeaderextends Lean.Elab.DefView, Lean.Elab.DefViewElabHeaderData : Type

DefView plus header elaboration data and snapshot.

• kind : DefKind
• ref : Syntax
• headerRef : Syntax
• modifiers : Modifiers
• declId : Syntax
• binders : Syntax
• type? : Option Syntax
• value : Syntax
• headerSnap? : Option (Language.SnapshotBundle (Option HeaderProcessedSnapshot))
• deriving? : Option (Array Syntax)
• shortDeclName : Name
• declName : Name
• levelNames : List Name
• binderIds : Array Syntax
• numParams : Nat
• type : Expr
• tacSnap? : Option (Language.SnapshotBundle Tactic.TacticParsedSnapshot)

  Snapshot for incremental processing of top-level tactic block, if any.

  Invariant: if the bundle's old? is set, then the state up to the start of the tactic block is unchanged, i.e. reuse is possible.

• bodySnap? : Option (Language.SnapshotBundle (Option BodyProcessedSnapshot))

  Snapshot for incremental processing of definition body.

  Invariant: if the bundle's old? is set, then elaboration of the body is guaranteed to result in the same elaboration result and state, i.e. reuse is possible.

instance Lean.Elab.instInhabitedDefViewElabHeader : Inhabited DefViewElabHeader

Equations

• Lean.Elab.instInhabitedDefViewElabHeader = { default := { toDefView := default, toDefViewElabHeaderData := default, tacSnap? := default, bodySnap? := default } }

def Lean.Elab.Term.failedToInferDefTypeErrorName : Name

The error name for "failed to infer definition type" errors.

We cannot use logNamedError here because the error is logged later, after attempting to synthesize metavariables, in logUnassignedUsingErrorInfos.

Equations

• Lean.Elab.Term.failedToInferDefTypeErrorName = `lean.inferDefTypeFailed

opaque Lean.Elab.Term.deprecated.oldSectionVars : Lean.Option Bool

opaque Lean.Elab.Term.linter.unusedSectionVars : Lean.Option Bool

opaque Lean.Elab.Term.debug.proofAsSorry : Lean.Option Bool

@[reducible, inline]

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 : UsedFVarsMap
• modified : Bool

@[reducible, inline]

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 FVarId) (usedFVarsMap : UsedFVarsMap) : UsedFVarsMap

Equations

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

@[reducible, inline]

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 LocalDecl
• localDecls : Array LocalDecl
• newLetDecls : Array LocalDecl
• exprArgs : Array Expr

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

• ref : Syntax
• localDecls : Array LocalDecl
• closed : Expr

  Expression used to replace occurrences of the let-rec FVarId.

• toLift : LetRecToLift

@[reducible, inline]

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 : Replacement) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr) : Replacement

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Term.MutualClosure.main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars mainVals : Array Expr) (letRecsToLift : List LetRecToLift) : TermElabM (Array 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.

structure Lean.Elab.Term.AsyncBodyInfo : Type

instance Lean.Elab.Term.instTypeNameAsyncBodyInfo : TypeName AsyncBodyInfo

Equations

• Lean.Elab.Term.instTypeNameAsyncBodyInfo = Lean.Elab.Term.inst✝

def Lean.Elab.Term.elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit

Equations

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

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

Equations

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

Note [Delayed-Assigned Metavariables in Free Variable Collection]

Nested declarations using let rec should compile correctly even when nested within expressions that are elaborated using delayed metavariable assignments, such as match expressions and tactic blocks. Previously, declaring a let rec within such an expression in the following fashion

def f x :=
  let rec g :=
    match ... with
    | pat =>
      let rec h := ... g ...
      ... x ...

where g depends on some free variable bound by f (like x above) would cause MutualClosure to fail to detect that transitive fvar dependency of h (which must pass it as an argument to g), leading to an unbound fvar in the body of h that was ultimately fed to the kernel. This occurred because MutualClosure processes let-recs from most to least nested. Initially, the body of g is an application of the delayed-assigned metavariable generated by match elaboration; the root metavariable of that delayed assignment is, in turn, assigned to an expression that refers to the mvar that will eventually be assigned to g once we process that declaration. Therefore, when we initially process the most-nested declaration h (before g), we cannot instantiate the match-expression mvar's delayed assignment (since the metavariable that will eventually be assigned to the yet-unprocessed g remains unassigned). Thus, we do not detect any of the fvar dependencies of g in the match body -- namely, that corresponding to x, which h should therefore also take as a parameter. This also caused a knock-on effect in certain situations, wherein h would compile as an axiom rather than as opaque, rendering f erroneously noncomputable.