Header elaboration data of a DefView
.
- shortDeclName : Name
Short name. Recall that all declarations in Lean 4 are potentially recursive. We use
shortDeclName
to refer to them atvalueStx
, and other declarations in the same mutual block. - declName : Name
Full name for this declaration. This is the name that will be added to the
Environment
. Universe level parameter names explicitly provided by the user.
Syntax objects for the binders occurring before
:
, we use them to populate theInfoTree
when elaboratingvalueStx
.- numParams : Nat
Number of parameters before
:
, it also includes auto-implicit parameters automatically added by Lean. - type : Expr
Type including parameters.
Instances For
Equations
Snapshot after processing of a definition body.
- state : Term.SavedState
State after elaboration.
- value : Expr
Elaboration result.
- moreSnaps : Array (Language.SnapshotTask Language.SnapshotTree)
Untyped snapshots from
logSnapshotTask
, saved at this level for cancellation.
Instances For
Snapshot after elaboration of a definition header.
- view : DefViewElabHeaderData
Elaboration results.
- state : Term.SavedState
Resulting elaboration state, including any environment additions.
Syntax of top-level tactic block if any, for checking reuse of
tacSnap?
.- tacSnap? : Option (Language.SnapshotTask Tactic.TacticParsedSnapshot)
Incremental execution of main tactic block, if any.
- bodyStx : Syntax
Syntax of definition body, for checking reuse of
bodySnap
. - bodySnap : Language.SnapshotTask (Option BodyProcessedSnapshot)
Result of body elaboration.
- moreSnaps : Array (Language.SnapshotTask Language.SnapshotTree)
Untyped snapshots from
logSnapshotTask
, saved at this level for cancellation.
Instances For
State before elaboration of a mutual definition.
- fullHeaderRef : Syntax
Unstructured syntax object comprising the full "header" of the definition from the modifiers (incl. docstring) up to the value, used for determining header elaboration reuse.
- headerProcessedSnap : Language.SnapshotTask (Option HeaderProcessedSnapshot)
Elaboration result, unless fatal exception occurred.
Instances For
Snapshot after syntax tree has been split into separate mutual def headers.
Definitions of this mutual block.
Instances For
- kind : DefKind
- ref : Syntax
- headerRef : Syntax
An unstructured syntax object that comprises the "header" of the definition, i.e. everything up to the value. Used as a more specific ref for header elaboration.
- modifiers : Modifiers
- declId : Syntax
- binders : Syntax
- value : Syntax
- headerSnap? : Option (Language.SnapshotBundle (Option HeaderProcessedSnapshot))
Snapshot for incremental processing of this definition.
Invariant: If the bundle's
old?
is set, then elaboration of the header is guaranteed to result in the same elaboration result and state, i.e. reuse is possible.