def Lean.Elab.instantiateMVarsProfiling (e : Expr) : MetaM Expr

Equations

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

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 } }

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.

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.Term.elabMutualDef.go (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.Term.elabMutualDef.processDeriving (views : Array DefView) (headers : Array DefViewElabHeader) : TermElabM PUnit

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.