- env : Lean.Environment
- fileMap : Lean.FileMap
- mctx : Lean.MetavarContext
- options : Lean.Options
- currNamespace : Lake.Name
- ngen : Lean.NameGenerator
Context after executing
Note that the term information collected during elaboration may contain metavariables, and their
assignments are stored at
The name of the elaborator that created this info.
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.
- 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.
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
- widgetId : Lake.Name
WidgetSourceobject 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
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
- 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
- context: Lean.Elab.ContextInfo → Lean.Elab.InfoTree → Lean.Elab.InfoTree
The context object is created by
- 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
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
InfoTree.goalsAt? which finds
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.
- enabled : Bool
Whether info trees should be recorded.
Map from holes in the infotree to child infotrees.
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.
assignments field is used to assign these holes.
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
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