- env : Lean.Environment
- fileMap : Lean.FileMap
- mctx : Lean.MetavarContext
- options : Lean.Options
- currNamespace : Lean.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.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.instInhabitedElabInfo = { default := { elaborator := default, stx := default } }
- lctx : Lean.LocalContext
- expr : Lean.Expr
- isBinder : Bool
Equations
- Lean.Elab.instInhabitedTermInfo = { default := { toElabInfo := default, lctx := default, expectedType? := default, expr := default, isBinder := default } }
Equations
- Lean.Elab.instInhabitedCommandInfo = { default := { toElabInfo := default } }
- dot: Lean.Elab.TermInfo → Option Lean.Syntax → Option Lean.Expr → Lean.Elab.CompletionInfo
- id: Lean.Syntax → Lean.Name → Bool → Lean.LocalContext → Option Lean.Expr → 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
Equations
- One or more equations did not get rendered due to their size.
Name of the projection.
projName : Lean.NameName of the field as written.
fieldName : Lean.Name- lctx : Lean.LocalContext
- val : Lean.Expr
- stx : Lean.Syntax
Equations
- Lean.Elab.instInhabitedFieldInfo = { default := { projName := default, fieldName := default, lctx := default, val := default, stx := default } }
- 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...`.
Equations
- Lean.Elab.instInhabitedTacticInfo = { default := { toElabInfo := default, mctxBefore := default, goalsBefore := default, mctxAfter := default, goalsAfter := default } }
- lctx : Lean.LocalContext
- stx : Lean.Syntax
- output : Lean.Syntax
Equations
- Lean.Elab.instInhabitedMacroExpansionInfo = { default := { lctx := default, stx := default, output := default } }
Equations
- Lean.Elab.instInhabitedCustomInfo = { default := { stx := default, json := default } }
Equations
- Lean.Elab.CustomInfo.format _fun_discr = let i := _fun_discr; Lean.format i.json
Equations
- Lean.Elab.instToFormatCustomInfo = { format := Lean.Elab.CustomInfo.format }
- 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
- ofFieldInfo: Lean.Elab.FieldInfo → Lean.Elab.Info
- ofCompletionInfo: Lean.Elab.CompletionInfo → Lean.Elab.Info
- ofCustomInfo: Lean.Elab.CustomInfo → Lean.Elab.Info
Header information for a node in InfoTree.
Equations
- Lean.Elab.instInhabitedInfo = { default := Lean.Elab.Info.ofTacticInfo default }
- context: Lean.Elab.ContextInfo → Lean.Elab.InfoTree → Lean.Elab.InfoTree
- node: Lean.Elab.Info → Std.PersistentArray Lean.Elab.InfoTree → Lean.Elab.InfoTree
- hole: Lean.MVarId → Lean.Elab.InfoTree
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
`hole`s which are filled in later in the same way that unassigned metavariables are.
Equations
- Lean.Elab.instInhabitedInfoTree = { default := Lean.Elab.InfoTree.node default default }
Whether info trees should be recorded.
enabled : BoolMap from holes in the infotree to child infotrees.
assignment : Std.PersistentHashMap Lean.MVarId Lean.Elab.InfoTreePending 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'.
Equations
- Lean.Elab.instInhabitedInfoState = { default := { enabled := default, assignment := default, trees := default } }
- getInfoState : m Lean.Elab.InfoState
- modifyInfoState : (Lean.Elab.InfoState → Lean.Elab.InfoState) → m Unit
Equations
- Lean.Elab.instMonadInfoTree = { getInfoState := liftM Lean.Elab.getInfoState, modifyInfoState := fun f => liftM (Lean.Elab.modifyInfoState f) }
Instantiate the holes on the given tree with the assignment table.
(analoguous to instantiating the metavariables in an expression)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.ContextInfo.toPPContext info lctx = { env := info.env, mctx := info.mctx, lctx := lctx, opts := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls }
Equations
- Lean.Elab.ContextInfo.ppSyntax info lctx stx = Lean.ppTerm (Lean.Elab.ContextInfo.toPPContext info lctx) stx
Equations
- Lean.Elab.TermInfo.runMetaM info ctx x = Lean.Elab.ContextInfo.runMetaM ctx info.lctx x
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.CommandInfo.format ctx info = pure (Lean.format "command @ " ++ Lean.format (Lean.Elab.formatElabInfo ctx info.toElabInfo) ++ Lean.format "")
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Helper function for propagating the tactic metavariable context to its children nodes.
We need this function because we preserve TacticInfo nodes during backtracking and their
children. Moreover, we backtrack the metavariable context to undo metavariable assignments.
TacticInfo nodes save the metavariable context before/after the tactic application, and
can be pretty printed without any extra information. This is not the case for TermInfo nodes.
Without this function, the formatting method would often fail when processing TermInfo nodes
that are children of TacticInfo nodes that have been preserved during backtracking.
Saving the metavariable context at TermInfo nodes is also not a good option because
at TermInfo creation time, the metavariable context often miss information, e.g.,
a TC problem has not been resolved, a postponed subterm has not been elaborated, etc.
See Term.SavedState.restore.
Equations
- One or more equations did not get rendered due to their size.
Returns the current array of InfoTrees and resets it to an empty array.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.pushInfoTree t = do let a ← Lean.Elab.getInfoState if a.enabled = true then Lean.Elab.modifyInfoTrees fun ts => Std.PersistentArray.push ts t else pure PUnit.unit
Equations
- One or more equations did not get rendered due to their size.
Equations
This does the same job as resolveGlobalConstNoOverload; resolving an identifier syntax to a unique fully resolved name or throwing if there are ambiguities. But also adds this resolved name to the infotree. This means that when you hover over a name in the sourcefile you will see the fully resolved name in the hover info.
Equations
- One or more equations did not get rendered due to their size.
Similar to resolveGlobalConstNoOverloadWithInfo, except if there are multiple name resolutions then it returns them as a list.
Equations
- One or more equations did not get rendered due to their size.
Use this to descend a node on the infotree that is being built.
It saves the current list of trees t₀ and resets it and then runs x >>= mkInfo, producing either an i : Info or a hole id.
Running x >>= mkInfo will modify the trees state and produce a new list of trees t₁.
In the i : Info case, t₁ become the children of a node node i t₁ that is appended to t₀.
Equations
- One or more equations did not get rendered due to their size.
Saves the current list of trees t₀, runs x to produce a new tree list t₁ and
runs mkInfoTree t₁ to get n : InfoTree and then restores the trees to be t₀ ++ [n].
Equations
- One or more equations did not get rendered due to their size.
Run x as a new child infotree node with header given by mkInfo.
Equations
- Lean.Elab.withInfoContext x mkInfo = Lean.Elab.withInfoTreeContext x fun trees => do let a ← mkInfo pure (Lean.Elab.InfoTree.node a trees)
Resets the trees state t₀, runs x to produce a new trees
state t₁ and sets the state to be t₀ ++ (InfoTree.context Γ <$> t₁)
where Γ is the context derived from the monad state.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.getInfoHoleIdAssignment? mvarId = do let a ← Lean.Elab.getInfoState pure (Std.PersistentHashMap.getOp a.assignment mvarId)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.enableInfoTree flag = Lean.Elab.modifyInfoState fun s => { enabled := flag, assignment := s.assignment, trees := s.trees }