def Lean.Language.Lean.pushOpt {α : Type u_1} (a? : Option α) (as : Array α) : Array α

Pushes a? into the array if it is some.

Equations

• Lean.Language.Lean.pushOpt (some a) as = as.push a
• Lean.Language.Lean.pushOpt none as = as

The hierarchy of Lean snapshot types

structure Lean.Language.Lean.CommandResultSnapshotextends Lean.Language.Snapshot : Type

Snapshot after command elaborator has returned. Also contains diagnostics from the elaborator's main task. Asynchronous elaboration tasks may not yet be finished.

• desc : String
• diagnostics : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• cmdState : Elab.Command.State

  Resulting elaboration state.

instance Lean.Language.Lean.instNonemptyCommandResultSnapshot : Nonempty CommandResultSnapshot

instance Lean.Language.Lean.instToSnapshotTreeCommandResultSnapshot : ToSnapshotTree CommandResultSnapshot

Equations

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

structure Lean.Language.Lean.CommandElaboratingSnapshotextends Lean.Language.Snapshot : Type

State before a command is elaborated. This is separate from CommandParsedSnapshot so that all snapshots belonging to a command are grouped below a task with the command's syntax tree.

• desc : String
• diagnostics : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• elabSnap : SnapshotTask DynamicSnapshot

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

• resultSnap : SnapshotTask CommandResultSnapshot

  State after command elaborator has returned.

• infoTreeSnap : SnapshotTask SnapshotLeaf

  State after all elaborator tasks are finished. In particular, contains the complete info tree.

• reportSnap : SnapshotTask SnapshotTree

  Additional, untyped snapshots used for reporting, not reuse.

instance Lean.Language.Lean.instNonemptyCommandElaboratingSnapshot : Nonempty CommandElaboratingSnapshot

instance Lean.Language.Lean.instToSnapshotTreeCommandElaboratingSnapshot : ToSnapshotTree CommandElaboratingSnapshot

Equations

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

def Lean.Language.Lean.instToSnapshotTreeCommandElaboratingSnapshot.go (s : CommandElaboratingSnapshot) : SnapshotTree

Equations

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

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 : CommandElaboratingSnapshot

  State before the command is elaborated. This snapshot is always fulfilled immediately.

• 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
• metaSnap : SnapshotTask SnapshotLeaf

  Holds produced diagnostics and info tree. Separate snapshot so that it can be tagged with the header syntax, which should not be done for this snapshot containing firstCmdSnap.

• 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
• metaSnap : SnapshotTask SnapshotLeaf

  Holds produced diagnostics. Separate snapshot so that it can be tagged with the header syntax, which should not be done for this snapshot containing firstCmdSnap.

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

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