The hierarchy of Lean snapshot types

structure Lean.Language.Lean.CommandFinishedSnapshotextends Lean.Language.Snapshot : Type

Snapshot after elaboration of the entire command.

• desc : String
• diagnostics : Lean.Language.Snapshot.Diagnostics
• infoTree? : Option Lean.Elab.InfoTree
• isFatal : Bool
• cmdState : Lean.Elab.Command.State

  Resulting elaboration state.

instance Lean.Language.Lean.instNonemptyCommandFinishedSnapshot : Nonempty Lean.Language.Lean.CommandFinishedSnapshot

Equations

• Lean.Language.Lean.instNonemptyCommandFinishedSnapshot = ⋯

instance Lean.Language.Lean.instToSnapshotTreeCommandFinishedSnapshot : Lean.Language.ToSnapshotTree Lean.Language.Lean.CommandFinishedSnapshot

Equations

• Lean.Language.Lean.instToSnapshotTreeCommandFinishedSnapshot = { toSnapshotTree := fun (s : Lean.Language.Lean.CommandFinishedSnapshot) => Lean.Language.SnapshotTree.mk s.toSnapshot #[] }

structure Lean.Language.Lean.CommandParsedSnapshotDataextends Lean.Language.Snapshot : Type

State after a command has been parsed.

• desc : String
• diagnostics : Lean.Language.Snapshot.Diagnostics
• infoTree? : Option Lean.Elab.InfoTree
• isFatal : Bool
• stx : Lean.Syntax

  Syntax tree of the command.

• parserState : Lean.Parser.ModuleParserState

  Resulting parser state.

• elabSnap : Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot

  Snapshot for incremental reporting and reuse during elaboration, type dependent on specific elaborator.

• finishedSnap : Lean.Language.SnapshotTask Lean.Language.Lean.CommandFinishedSnapshot

  State after processing is finished.

• tacticCache : IO.Ref Lean.Elab.Tactic.Cache

  Cache for save; to be replaced with incrementality.

instance Lean.Language.Lean.instNonemptyCommandParsedSnapshotData : Nonempty Lean.Language.Lean.CommandParsedSnapshotData

Equations

• Lean.Language.Lean.instNonemptyCommandParsedSnapshotData = ⋯

inductive Lean.Language.Lean.CommandParsedSnapshot : Type

State after a command has been parsed.

• mk: Lean.Language.Lean.CommandParsedSnapshotData → Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Lean.Language.Lean.CommandParsedSnapshot

  Creates a command parsed snapshot.

instance Lean.Language.Lean.instNonemptyCommandParsedSnapshot : Nonempty Lean.Language.Lean.CommandParsedSnapshot

Equations

• Lean.Language.Lean.instNonemptyCommandParsedSnapshot = ⋯

@[reducible, inline]

abbrev Lean.Language.Lean.CommandParsedSnapshot.data : Lean.Language.Lean.CommandParsedSnapshot → Lean.Language.Lean.CommandParsedSnapshotData

The snapshot data.

Equations

• x.data = match x with | Lean.Language.Lean.CommandParsedSnapshot.mk data nextCmdSnap? => data

@[reducible, inline]

abbrev Lean.Language.Lean.CommandParsedSnapshot.nextCmdSnap? : Lean.Language.Lean.CommandParsedSnapshot → Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)

Next command, unless this is a terminal command.

Equations

• x.nextCmdSnap? = match x with | Lean.Language.Lean.CommandParsedSnapshot.mk data next? => next?

instance Lean.Language.Lean.instToSnapshotTreeCommandParsedSnapshot : Lean.Language.ToSnapshotTree Lean.Language.Lean.CommandParsedSnapshot

Equations

• Lean.Language.Lean.instToSnapshotTreeCommandParsedSnapshot = { toSnapshotTree := Lean.Language.Lean.instToSnapshotTreeCommandParsedSnapshot.go }

partial def Lean.Language.Lean.instToSnapshotTreeCommandParsedSnapshot.go (s : Lean.Language.Lean.CommandParsedSnapshot) : Lean.Language.SnapshotTree

structure Lean.Language.Lean.HeaderProcessedState : Type

State after successful importing.

• cmdState : Lean.Elab.Command.State

  The resulting initial elaboration state.

• firstCmdSnap : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot

  First command task (there is always at least a terminal command).

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

State after the module header has been processed including imports.

• desc : String
• diagnostics : Lean.Language.Snapshot.Diagnostics
• infoTree? : Option Lean.Elab.InfoTree
• isFatal : Bool
• result? : Option Lean.Language.Lean.HeaderProcessedState

  State after successful importing.

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

Equations

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

structure Lean.Language.Lean.HeaderParsedState : Type

State after successfully parsing the module header.

• parserState : Lean.Parser.ModuleParserState

  Resulting parser state.

• processedSnap : Lean.Language.SnapshotTask Lean.Language.Lean.HeaderProcessedSnapshot

  Header processing task.

structure Lean.Language.Lean.HeaderParsedSnapshotextends Lean.Language.Snapshot : Type

State after the module header has been parsed.

• desc : String
• diagnostics : Lean.Language.Snapshot.Diagnostics
• infoTree? : Option Lean.Elab.InfoTree
• isFatal : Bool
• ictx : Lean.Parser.InputContext

  Parser input context supplied by the driver, stored here for incremental parsing.

• stx : Lean.Syntax

  Resulting syntax tree.

• result? : Option Lean.Language.Lean.HeaderParsedState

  State after successful parsing.

• cancelTk? : Option IO.CancelToken

  Cancellation token for interrupting processing of this run.

instance Lean.Language.Lean.instToSnapshotTreeHeaderParsedSnapshot : Lean.Language.ToSnapshotTree Lean.Language.Lean.HeaderParsedSnapshot

Equations

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

def Lean.Language.Lean.HeaderParsedSnapshot.processedResult (snap : Lean.Language.Lean.HeaderParsedSnapshot) : Lean.Language.SnapshotTask (Option Lean.Language.Lean.HeaderProcessedState)

Shortcut accessor to the final header state, if successful.

Equations

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

@[reducible, inline]

abbrev Lean.Language.Lean.InitialSnapshot : Type

Initial snapshot of the Lean language processor: a "header parsed" snapshot.

Equations

• Lean.Language.Lean.InitialSnapshot = Lean.Language.Lean.HeaderParsedSnapshot