structure Lean.Elab.CommandContextInfo : Type

Context after executing liftTermElabM. Note that the term information collected during elaboration may contain metavariables, and their assignments are stored at mctx.

• env : Lean.Environment
• fileMap : Lean.FileMap
• mctx : Lean.MetavarContext
• options : Lean.Options
• currNamespace : Lean.Name
• openDecls : List Lean.OpenDecl
• ngen : Lean.NameGenerator

structure Lean.Elab.ContextInfoextends Lean.Elab.CommandContextInfo : Type

Context from the root of the InfoTree up to this node. Note that the term information collected during elaboration may contain metavariables, and their assignments are stored at mctx.

• env : Lean.Environment
• fileMap : Lean.FileMap
• mctx : Lean.MetavarContext
• options : Lean.Options
• currNamespace : Lean.Name
• openDecls : List Lean.OpenDecl
• ngen : Lean.NameGenerator
• parentDecl? : Option Lean.Name

inductive Lean.Elab.PartialContextInfo : Type

Context for a sub-InfoTree.

Within InfoTree, this must fulfill the invariant that every non-commandCtx PartialContextInfo node is always contained within a commandCtx node.

• commandCtx: Lean.Elab.CommandContextInfo → Lean.Elab.PartialContextInfo
• parentDeclCtx: Lean.Name → Lean.Elab.PartialContextInfo

  Context for the name of the declaration that surrounds nodes contained within this context node. For example, this makes the name of the surrounding declaration available in InfoTree nodes corresponding to the terms within the declaration.

structure Lean.Elab.ElabInfo : Type

Base structure for TermInfo, CommandInfo and TacticInfo.

• elaborator : Lean.Name

  The name of the elaborator that created this info.

• stx : Lean.Syntax

  The piece of syntax that the elaborator created this info for. Note that this also implicitly stores the code position in the syntax's SourceInfo.

instance Lean.Elab.instInhabitedElabInfo : Inhabited Lean.Elab.ElabInfo

Equations

• Lean.Elab.instInhabitedElabInfo = { default := { elaborator := default, stx := default } }

structure Lean.Elab.TermInfoextends Lean.Elab.ElabInfo : Type

• elaborator : Lean.Name
• stx : Lean.Syntax
• lctx : Lean.LocalContext
• expectedType? : Option Lean.Expr
• expr : Lean.Expr
• isBinder : Bool

instance Lean.Elab.instInhabitedTermInfo : Inhabited Lean.Elab.TermInfo

Equations

• Lean.Elab.instInhabitedTermInfo = { default := { toElabInfo := default, lctx := default, expectedType? := default, expr := default, isBinder := default } }

structure Lean.Elab.CommandInfoextends Lean.Elab.ElabInfo : Type

• elaborator : Lean.Name
• stx : Lean.Syntax

instance Lean.Elab.instInhabitedCommandInfo : Inhabited Lean.Elab.CommandInfo

Equations

• Lean.Elab.instInhabitedCommandInfo = { default := { toElabInfo := default } }

inductive Lean.Elab.CompletionInfo : Type

A completion is an item that appears in the IntelliSense box that appears as you type.

• dot: Lean.Elab.TermInfo → Option Lean.Expr → Lean.Elab.CompletionInfo
• id: Lean.Syntax → Lean.Name → Bool → Lean.LocalContext → Option Lean.Expr → Lean.Elab.CompletionInfo
• dotId: Lean.Syntax → Lean.Name → Lean.LocalContext → Option Lean.Expr → Lean.Elab.CompletionInfo
• fieldId: Lean.Syntax → Lean.Name → Lean.LocalContext → Lean.Name → Lean.Elab.CompletionInfo
• namespaceId: Lean.Syntax → Lean.Elab.CompletionInfo
• option: Lean.Syntax → Lean.Elab.CompletionInfo
• endSection: Lean.Syntax → List String → Lean.Elab.CompletionInfo
• tactic: Lean.Syntax → Lean.Elab.CompletionInfo

structure Lean.Elab.OptionInfo : Type

Info for an option reference (e.g. in set_option).

• stx : Lean.Syntax
• optionName : Lean.Name
• declName : Lean.Name

structure Lean.Elab.FieldInfo : Type

• projName : Lean.Name

  Name of the projection.

• fieldName : Lean.Name

  Name of the field as written.

• lctx : Lean.LocalContext
• val : Lean.Expr
• stx : Lean.Syntax

instance Lean.Elab.instInhabitedFieldInfo : Inhabited Lean.Elab.FieldInfo

Equations

• Lean.Elab.instInhabitedFieldInfo = { default := { projName := default, fieldName := default, lctx := default, val := default, stx := default } }

structure Lean.Elab.TacticInfoextends Lean.Elab.ElabInfo : Type

The information needed to render the tactic state in the infoview.

We store the list of goals before and after the execution of a tactic. We also store the metavariable context at each time since we want metavariables unassigned at tactic execution time to be displayed as ?m....

• elaborator : Lean.Name
• stx : Lean.Syntax
• mctxBefore : Lean.MetavarContext
• goalsBefore : List Lean.MVarId
• mctxAfter : Lean.MetavarContext
• goalsAfter : List Lean.MVarId

instance Lean.Elab.instInhabitedTacticInfo : Inhabited Lean.Elab.TacticInfo

Equations

• Lean.Elab.instInhabitedTacticInfo = { default := { toElabInfo := default, mctxBefore := default, goalsBefore := default, mctxAfter := default, goalsAfter := default } }

structure Lean.Elab.MacroExpansionInfo : Type

• lctx : Lean.LocalContext
• stx : Lean.Syntax
• output : Lean.Syntax

instance Lean.Elab.instInhabitedMacroExpansionInfo : Inhabited Lean.Elab.MacroExpansionInfo

Equations

• Lean.Elab.instInhabitedMacroExpansionInfo = { default := { lctx := default, stx := default, output := default } }

structure Lean.Elab.CustomInfo : Type

Dynamic info for custom use cases.

• stx : Lean.Syntax
• value : Dynamic

structure Lean.Elab.UserWidgetInfoextends Lean.Widget.WidgetInstance : Type

Information about a user widget associated with a syntactic span. This must be a panel widget. A panel widget is a widget that can be displayed in the infoview alongside the goal state.

• id : Lean.Name
• javascriptHash : UInt64
• props : StateM Lean.Server.RpcObjectStore Lean.Json
• stx : Lean.Syntax

structure Lean.Elab.FVarAliasInfo : Type

Specifies that the given free variables should be considered semantically identical. The free variable baseId might not be in the current local context because it has been cleared. Used for e.g. connecting variables before and after match generalization.

• userName : Lean.Name
• id : Lean.FVarId
• baseId : Lean.FVarId

structure Lean.Elab.FieldRedeclInfo : Type

Contains the syntax of an identifier which is part of a field redeclaration, like:

structure Foo := x : Nat
structure Bar extends Foo :=
  x := 0
--^ here

• stx : Lean.Syntax

structure Lean.Elab.OmissionInfoextends Lean.Elab.TermInfo : Type

Denotes information for the term ⋯ that is emitted by the delaborator when omitting a term due to pp.deepTerms false or pp.proofs false. Omission needs to be treated differently from regular terms because it has to be delaborated differently in Lean.Widget.InteractiveDiagnostics.infoToInteractive: Regular terms are delaborated explicitly, whereas omitted terms are simply to be expanded with regular delaboration settings.

• elaborator : Lean.Name
• stx : Lean.Syntax
• lctx : Lean.LocalContext
• expectedType? : Option Lean.Expr
• expr : Lean.Expr
• isBinder : Bool
• reason : String

inductive Lean.Elab.Info : Type

Header information for a node in InfoTree.

• ofTacticInfo: Lean.Elab.TacticInfo → Lean.Elab.Info
• ofTermInfo: Lean.Elab.TermInfo → Lean.Elab.Info
• ofCommandInfo: Lean.Elab.CommandInfo → Lean.Elab.Info
• ofMacroExpansionInfo: Lean.Elab.MacroExpansionInfo → Lean.Elab.Info
• ofOptionInfo: Lean.Elab.OptionInfo → Lean.Elab.Info
• ofFieldInfo: Lean.Elab.FieldInfo → Lean.Elab.Info
• ofCompletionInfo: Lean.Elab.CompletionInfo → Lean.Elab.Info
• ofUserWidgetInfo: Lean.Elab.UserWidgetInfo → Lean.Elab.Info
• ofCustomInfo: Lean.Elab.CustomInfo → Lean.Elab.Info
• ofFVarAliasInfo: Lean.Elab.FVarAliasInfo → Lean.Elab.Info
• ofFieldRedeclInfo: Lean.Elab.FieldRedeclInfo → Lean.Elab.Info
• ofOmissionInfo: Lean.Elab.OmissionInfo → Lean.Elab.Info

instance Lean.Elab.instInhabitedInfo : Inhabited Lean.Elab.Info

Equations

• Lean.Elab.instInhabitedInfo = { default := Lean.Elab.Info.ofTacticInfo default }

inductive Lean.Elab.InfoTree : Type

The InfoTree is a structure that is generated during elaboration and used by the language server to look up information about objects at particular points in the Lean document. For example, tactic information and expected type information in the infoview and information about completions.

The infotree consists of nodes which may have child nodes. Each node has an Info object that contains details about what kind of information is present. Each Info object also contains a Syntax instance, this is used to map positions in the Lean document to particular info objects.

An example of a function that extracts information from an infotree for a given position is InfoTree.goalsAt? which finds TacticInfo.

Information concerning expressions requires that a context also be saved. context nodes store a local context that is used to process expressions in nodes below.

Because the info tree is generated during elaboration, some parts of the infotree for a particular piece of syntax may not be ready yet. Hence InfoTree supports metavariable-like holes which are filled in later in the same way that unassigned metavariables are.

• context: Lean.Elab.PartialContextInfo → Lean.Elab.InfoTree → Lean.Elab.InfoTree

  The context object is created at appropriate points during elaboration

• node: Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → Lean.Elab.InfoTree

  The children contain information for nested term elaboration and tactic evaluation

• hole: Lean.MVarId → Lean.Elab.InfoTree

  The elaborator creates holes (aka metavariables) for tactics and postponed terms

instance Lean.Elab.instInhabitedInfoTree : Inhabited Lean.Elab.InfoTree

Equations

• Lean.Elab.instInhabitedInfoTree = { default := Lean.Elab.InfoTree.node default default }

structure Lean.Elab.InfoState : Type

This structure is the state that is being used to build an InfoTree object. During elaboration, some parts of the info tree may be holes which need to be filled later. The assignments field is used to assign these holes. The trees field is a list of pending child trees for the infotree node currently being built.

You should not need to use InfoState directly, instead infotrees should be built with the help of the methods here such as pushInfoLeaf to create leaf nodes and withInfoContext to create a nested child node.

To see how trees is used, look at the function body of withInfoContext'.

• enabled : Bool

  Whether info trees should be recorded.

• assignment : Lean.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree

  Map from holes in the infotree to child infotrees.

• trees : Lean.PersistentArray Lean.Elab.InfoTree

  Pending child trees of a node.

instance Lean.Elab.instInhabitedInfoState : Inhabited Lean.Elab.InfoState

Equations

• Lean.Elab.instInhabitedInfoState = { default := { enabled := default, assignment := default, trees := default } }

class Lean.Elab.MonadInfoTree (m : Type → Type) : Type

• getInfoState : m Lean.Elab.InfoState
• modifyInfoState : (Lean.Elab.InfoState → Lean.Elab.InfoState) → m Unit

instance Lean.Elab.instMonadInfoTreeOfMonadLift {m n : Type → Type} [MonadLift m n] [Lean.Elab.MonadInfoTree m] : Lean.Elab.MonadInfoTree n

Equations

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

def Lean.Elab.setInfoState {m : Type → Type} [Lean.Elab.MonadInfoTree m] (s : Lean.Elab.InfoState) : m Unit

Equations

• Lean.Elab.setInfoState s = Lean.Elab.modifyInfoState fun (x : Lean.Elab.InfoState) => s

class Lean.Elab.MonadParentDecl (m : Type → Type) : Type

• getParentDeclName? : m (Option Lean.Name)