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
• traces : Lean.TraceState
• isFatal : Bool
• cmdState : Lean.Elab.Command.State

  Resulting elaboration state.

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

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

Equations

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

structure Lean.Language.Lean.CommandParsedSnapshotextends Lean.Language.Snapshot : Type

State after a command has been parsed.

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

• reportSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotTree

  Additional, untyped snapshots used for reporting, not reuse.

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

  Cache for save; to be replaced with incrementality.

• nextCmdSnap? : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)

  Next command, unless this is a terminal command.

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

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
• traces : Lean.TraceState
• 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
• traces : Lean.TraceState
• 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