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
• docString? : Option (TSyntax `Lean.Parser.Command.docComment × Bool)
• 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.

def Lean.Elab.instInhabitedDefViewElabHeader.default : DefViewElabHeader

instance Lean.Elab.instInhabitedDefViewElabHeader : Inhabited DefViewElabHeader

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.

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.

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

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

@[reducible, inline]

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

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.

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

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

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

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

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

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

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

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

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

structure Lean.Elab.Term.AsyncBodyInfo : Type

instance Lean.Elab.Term.instTypeNameAsyncBodyInfo : TypeName AsyncBodyInfo

opaque Lean.Elab.Term.warn.exposeOnPrivate : Lean.Option Bool

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

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

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.