inductive Lean.Elab.DefKind : Type

• def : DefKind
• instance : DefKind
• theorem : DefKind
• example : DefKind
• opaque : DefKind
• abbrev : DefKind

def Lean.Elab.instInhabitedDefKind.default : DefKind

Equations

• Lean.Elab.instInhabitedDefKind.default = Lean.Elab.DefKind.def

instance Lean.Elab.instInhabitedDefKind : Inhabited DefKind

Equations

• Lean.Elab.instInhabitedDefKind = { default := Lean.Elab.instInhabitedDefKind.default }

def Lean.Elab.instBEqDefKind.beq : DefKind → DefKind → Bool

Equations

• Lean.Elab.instBEqDefKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lean.Elab.instBEqDefKind : BEq DefKind

Equations

• Lean.Elab.instBEqDefKind = { beq := Lean.Elab.instBEqDefKind.beq }

def Lean.Elab.DefKind.isTheorem : DefKind → Bool

Equations

• Lean.Elab.DefKind.theorem.isTheorem = true
• x✝.isTheorem = false

def Lean.Elab.DefKind.isExample : DefKind → Bool

Equations

• Lean.Elab.DefKind.example.isExample = true
• x✝.isExample = false

structure Lean.Elab.DefViewElabHeaderData : Type

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 at valueStx, 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.

• levelNames : List Name

  Universe level parameter names explicitly provided by the user.

• binderIds : Array Syntax

  Syntax objects for the binders occurring before :, we use them to populate the InfoTree when elaborating valueStx.

• numParams : Nat

  Number of parameters before :, it also includes auto-implicit parameters automatically added by Lean.

• type : Expr

  Type including parameters.

def Lean.Elab.instInhabitedDefViewElabHeaderData.default : DefViewElabHeaderData

Equations

• Lean.Elab.instInhabitedDefViewElabHeaderData.default = { shortDeclName := default, declName := default, levelNames := default, binderIds := default, numParams := default, type := default }

instance Lean.Elab.instInhabitedDefViewElabHeaderData : Inhabited DefViewElabHeaderData

Equations

• Lean.Elab.instInhabitedDefViewElabHeaderData = { default := Lean.Elab.instInhabitedDefViewElabHeaderData.default }

structure Lean.Elab.BodyProcessedSnapshotextends Lean.Language.Snapshot : Type

Snapshot after processing of a definition body.

• desc : String
• diagnostics : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• 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.

instance Lean.Elab.instNonemptyBodyProcessedSnapshot : Nonempty BodyProcessedSnapshot

instance Lean.Elab.instToSnapshotTreeBodyProcessedSnapshot : Language.ToSnapshotTree BodyProcessedSnapshot

Equations

• Lean.Elab.instToSnapshotTreeBodyProcessedSnapshot = { toSnapshotTree := fun (s : Lean.Elab.BodyProcessedSnapshot) => { element := s.toSnapshot, children := s.moreSnaps } }

structure Lean.Elab.HeaderProcessedSnapshotextends Lean.Language.Snapshot : Type

Snapshot after elaboration of a definition header.

• desc : String
• diagnostics : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• view : DefViewElabHeaderData

  Elaboration results.

• state : Term.SavedState

  Resulting elaboration state, including any environment additions.

• tacStx? : Option Syntax

  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.

instance Lean.Elab.instNonemptyHeaderProcessedSnapshot : Nonempty HeaderProcessedSnapshot

instance Lean.Elab.instToSnapshotTreeHeaderProcessedSnapshot : Language.ToSnapshotTree HeaderProcessedSnapshot

Equations

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

structure Lean.Elab.DefParsed : Type

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.

instance Lean.Elab.instNonemptyDefParsed : Nonempty DefParsed

structure Lean.Elab.DefsParsedSnapshotextends Lean.Language.Snapshot : Type

Snapshot after syntax tree has been split into separate mutual def headers.

• desc : String
• diagnostics : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• defs : Array DefParsed

  Definitions of this mutual block.

instance Lean.Elab.instNonemptyDefsParsedSnapshot : Nonempty DefsParsedSnapshot

instance Lean.Elab.instTypeNameDefsParsedSnapshot : TypeName DefsParsedSnapshot

Equations

• Lean.Elab.instTypeNameDefsParsedSnapshot = Lean.Elab.inst✝

instance Lean.Elab.instToSnapshotTreeDefsParsedSnapshot : Language.ToSnapshotTree DefsParsedSnapshot

Equations

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

structure Lean.Elab.DefView : Type

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

  The docstring, if present, and whether it's Verso

• 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.

• deriving? : Option (Array Syntax)

instance Lean.Elab.instInhabitedDefView : Inhabited DefView

Equations

• Lean.Elab.instInhabitedDefView = { default := Lean.Elab.instInhabitedDefView.default }

def Lean.Elab.instInhabitedDefView.default : DefView

Equations

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

def Lean.Elab.DefView.isInstance (view : DefView) : Bool

Equations

• view.isInstance = view.modifiers.attrs.any fun (attr : Lean.Elab.Attribute) => attr.name == `instance

def Lean.Elab.DefView.markDefEq (view : DefView) : DefView

Prepends the defeq attribute, removing existing ones if there are any

Equations

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

def Lean.Elab.Command.mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView

Equations

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

def Lean.Elab.Command.mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView

Equations

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

def Lean.Elab.Command.mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView

Equations

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

def Lean.Elab.Command.mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView

Equations

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

def Lean.Elab.Command.mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView

Equations

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

def Lean.Elab.Command.mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView

Equations

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

def Lean.Elab.Command.isDefLike (stx : Syntax) : Bool

Equations

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

def Lean.Elab.Command.mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView

Equations

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