inductive Lean.Elab.DefKind : Type

• def: Lean.Elab.DefKind
• instance: Lean.Elab.DefKind
• theorem: Lean.Elab.DefKind
• example: Lean.Elab.DefKind
• opaque: Lean.Elab.DefKind
• abbrev: Lean.Elab.DefKind

Instances For

• Lean.Elab.instBEqDefKind
• Lean.Elab.instInhabitedDefKind

instance Lean.Elab.instInhabitedDefKind : Inhabited Lean.Elab.DefKind

Equations

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

instance Lean.Elab.instBEqDefKind : BEq Lean.Elab.DefKind

Equations

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

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

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

Equations

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

structure Lean.Elab.DefViewElabHeaderData : Type

Header elaboration data of a DefView.

• shortDeclName : Lean.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 : Lean.Name

  Full name for this declaration. This is the name that will be added to the Environment.

• levelNames : List Lean.Name

  Universe level parameter names explicitly provided by the user.

• binderIds : Array Lean.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 : Lean.Expr

  Type including parameters.

Instances For

• Lean.Elab.instInhabitedDefViewElabHeaderData

instance Lean.Elab.instInhabitedDefViewElabHeaderData : Inhabited Lean.Elab.DefViewElabHeaderData

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

Snapshot after processing of a definition body.

• desc : String
• diagnostics : Lean.Language.Snapshot.Diagnostics
• infoTree? : Option Lean.Elab.InfoTree
• traces : Lean.TraceState
• isFatal : Bool
• state : Lean.Elab.Term.SavedState

  State after elaboration.

• value : Lean.Expr

  Elaboration result.

Instances For

• Lean.Elab.instToSnapshotTreeBodyProcessedSnapshot

theorem Lean.Elab.instNonemptyBodyProcessedSnapshot : Nonempty Lean.Elab.BodyProcessedSnapshot

instance Lean.Elab.instToSnapshotTreeBodyProcessedSnapshot : Lean.Language.ToSnapshotTree Lean.Elab.BodyProcessedSnapshot

Equations

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

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

Snapshot after elaboration of a definition header.

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

  Elaboration results.

• state : Lean.Elab.Term.SavedState

  Resulting elaboration state, including any environment additions.

• tacStx? : Option Lean.Syntax

  Syntax of top-level tactic block if any, for checking reuse of tacSnap?.

• tacSnap? : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)

  Incremental execution of main tactic block, if any.

• bodyStx : Lean.Syntax

  Syntax of definition body, for checking reuse of bodySnap.

• bodySnap : Lean.Language.SnapshotTask (Option Lean.Elab.BodyProcessedSnapshot)

  Result of body elaboration.

Instances For

• Lean.Elab.instToSnapshotTreeHeaderProcessedSnapshot

theorem Lean.Elab.instNonemptyHeaderProcessedSnapshot : Nonempty Lean.Elab.HeaderProcessedSnapshot

instance Lean.Elab.instToSnapshotTreeHeaderProcessedSnapshot : Lean.Language.ToSnapshotTree Lean.Elab.HeaderProcessedSnapshot

structure Lean.Elab.DefParsed : Type

State before elaboration of a mutual definition.

• fullHeaderRef : Lean.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 : Lean.Language.SnapshotTask (Option Lean.Elab.HeaderProcessedSnapshot)

  Elaboration result, unless fatal exception occurred.

theorem Lean.Elab.instNonemptyDefParsed : Nonempty Lean.Elab.DefParsed

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

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

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

  Definitions of this mutual block.

Instances For

• Lean.Elab.instToSnapshotTreeDefsParsedSnapshot
• Lean.Elab.instTypeNameDefsParsedSnapshot

theorem Lean.Elab.instNonemptyDefsParsedSnapshot : Nonempty Lean.Elab.DefsParsedSnapshot

instance Lean.Elab.instTypeNameDefsParsedSnapshot : TypeName Lean.Elab.DefsParsedSnapshot

Equations

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

instance Lean.Elab.instToSnapshotTreeDefsParsedSnapshot : Lean.Language.ToSnapshotTree Lean.Elab.DefsParsedSnapshot

structure Lean.Elab.DefView : Type

• kind : Lean.Elab.DefKind
• ref : Lean.Syntax
• headerRef : Lean.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 : 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))

  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 Lean.Syntax)

Instances For

• Lean.Elab.instInhabitedDefView

instance Lean.Elab.instInhabitedDefView : Inhabited Lean.Elab.DefView

Equations

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

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

Equations

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

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

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

Equations

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

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

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

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

Equations

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

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

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

Equations

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

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