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

DefView plus header elaboration data and snapshot.

• kind : Lean.Elab.DefKind
• ref : Lean.Syntax
• headerRef : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• declId : Lean.Syntax
• binders : Lean.Syntax
• type? : Option Lean.Syntax
• value : Lean.Syntax
• headerSnap? : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.HeaderProcessedSnapshot))
• deriving? : Option (Array Lean.Syntax)
• shortDeclName : Lake.Name
• declName : Lake.Name
• levelNames : List Lake.Name
• binderIds : Array Lean.Syntax
• numParams : Nat
• type : Lean.Expr
• tacSnap? : Option (Lean.Language.SnapshotBundle Lean.Elab.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 (Lean.Language.SnapshotBundle (Option Lean.Elab.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.

Instances For

• Lean.Elab.instInhabitedDefViewElabHeader

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

Equations

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

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

Equations

• Lean.Elab.Term.instantiateMVarsProfiling e = do let __do_lift ← Lean.getOptions Lean.profileitM Lean.Exception (toString "instantiate metavars") __do_lift (Lean.instantiateMVars e)

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

opaque Lean.Elab.Term.linter.unusedSectionVars : 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 : Lean.Elab.Term.MutualClosure.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 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.

@[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 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

@[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 : 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

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

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

Equations

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

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.elabMutualDef (vars : Array Lean.Expr) (sc : Lean.Elab.Command.Scope) (views : Array Lean.Elab.DefView) : 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) (sc : Lean.Elab.Command.Scope) (views : Array Lean.Elab.DefView) : 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 PUnit

Equations

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

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

Equations

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