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 : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• cmdState : Elab.Command.State

  Resulting elaboration state.

instance Lean.Language.Lean.instNonemptyCommandFinishedSnapshot : Nonempty CommandFinishedSnapshot

instance Lean.Language.Lean.instToSnapshotTreeCommandFinishedSnapshot : ToSnapshotTree 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 : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• stx : Syntax

  Syntax tree of the command.

• parserState : Parser.ModuleParserState

  Resulting parser state.

• elabSnap : SnapshotTask DynamicSnapshot

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

• finishedSnap : SnapshotTask CommandFinishedSnapshot

  State after processing is finished.

• reportSnap : SnapshotTask SnapshotTree

  Additional, untyped snapshots used for reporting, not reuse.

• tacticCache : IO.Ref Elab.Tactic.Cache

  Cache for save; to be replaced with incrementality.

• nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot)

  Next command, unless this is a terminal command.

instance Lean.Language.Lean.instNonemptyCommandParsedSnapshot : Nonempty CommandParsedSnapshot

instance Lean.Language.Lean.instToSnapshotTreeCommandParsedSnapshot : ToSnapshotTree CommandParsedSnapshot

Equations

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

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

structure Lean.Language.Lean.HeaderProcessedState : Type

State after successful importing.

• cmdState : Elab.Command.State

  The resulting initial elaboration state.

• firstCmdSnap : SnapshotTask 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 : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• result? : Option HeaderProcessedState

  State after successful importing.

instance Lean.Language.Lean.instToSnapshotTreeHeaderProcessedSnapshot : ToSnapshotTree 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 : Parser.ModuleParserState

  Resulting parser state.

• processedSnap : SnapshotTask HeaderProcessedSnapshot

  Header processing task.

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

State after the module header has been parsed.

• desc : String
• diagnostics : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• ictx : Parser.InputContext

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

• stx : Syntax

  Resulting syntax tree.

• result? : Option HeaderParsedState

  State after successful parsing.

• cancelTk? : Option IO.CancelToken

  Cancellation token for interrupting processing of this run.

instance Lean.Language.Lean.instToSnapshotTreeHeaderParsedSnapshot : ToSnapshotTree HeaderParsedSnapshot

Equations

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

def Lean.Language.Lean.HeaderParsedSnapshot.processedResult (snap : HeaderParsedSnapshot) : SnapshotTask (Option 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