structure Lean.Elab.ContextInfo : Type

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

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

structure Lean.Elab.ElabInfo : Type

• elaborator : Lake.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.

Base structure for TermInfo, CommandInfo and TacticInfo.

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 : Lake.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

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

Equations

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

inductive Lean.Elab.CompletionInfo : Type

• dot: Lean.Elab.TermInfo → Option Lean.Syntax → Option Lean.Expr → Lean.Elab.CompletionInfo
• id: Lean.Syntax → Lake.Name → Bool → Lean.LocalContext → Option Lean.Expr → Lean.Elab.CompletionInfo
• dotId: Lean.Syntax → Lake.Name → Lean.LocalContext → Option Lean.Expr → Lean.Elab.CompletionInfo
• fieldId: Lean.Syntax → Lake.Name → Lean.LocalContext → Lake.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 → List Lean.MVarId → Lean.Elab.CompletionInfo

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

structure Lean.Elab.OptionInfo : Type

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

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

structure Lean.Elab.FieldInfo : Type

• projName : Lake.Name

  Name of the projection.

• fieldName : Lake.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

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

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

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

• stx : Lean.Syntax
• value : Dynamic

Dynamic info for custom use cases.

structure Lean.Elab.UserWidgetInfo : Type

• stx : Lean.Syntax
• widgetId : Lake.Name

  Id of WidgetSource object to use.

• props : Lean.Json

  Json representing the props to be loaded in to the component.

An info that represents a user-widget. User-widgets are custom pieces of code that run on the editor client. You can learn about user widgets at src/Lean/Widget/UserWidget

instance Lean.Elab.instInhabitedUserWidgetInfo : Inhabited Lean.Elab.UserWidgetInfo

Equations

• Lean.Elab.instInhabitedUserWidgetInfo = { default := { stx := default, widgetId := default, props := default } }

structure Lean.Elab.FVarAliasInfo : Type

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

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.

structure Lean.Elab.FieldRedeclInfo : Type

• stx : Lean.Syntax

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

inductive Lean.Elab.Info : Type

• 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

Header information for a node in InfoTree.

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

Equations

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

inductive Lean.Elab.InfoTree : Type

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

  The context object is created by liftTermElabM at Command.lean

• 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

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.

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

Equations

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

structure Lean.Elab.InfoState : Type

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

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

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.instMonadInfoTree {m : Type → Type} {n : Type → Type} [MonadLift m n] [Lean.Elab.MonadInfoTree m] : Lean.Elab.MonadInfoTree n

Equations

• Lean.Elab.instMonadInfoTree = { getInfoState := liftM Lean.Elab.getInfoState, modifyInfoState := fun f => liftM (Lean.Elab.modifyInfoState f) }

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 => s