Equations
Instances For
Equations
Instances For
Merges the inner
partial context into the outer
context s.t. fields of the inner
context
overwrite fields of the outer
context. Panics if the invariant described in the documentation
for PartialContextInfo
is violated.
When traversing an InfoTree
, this function should be used to combine the context of outer
nodes with the partial context of their subtrees. This ensures that the traversal has the context
from the inner node to the root node of the InfoTree
available, with partial contexts of
inner nodes taking priority over contexts of outer nodes.
Equations
Instances For
Obtains the LocalContext
from this CompletionInfo
if available and yields an empty context
otherwise.
Equations
Instances For
Instantiate the holes on the given tree
with the assignment table.
(analogous to instantiating the metavariables in an expression)
Applies s.lazyAssignment
to s.trees
, asynchronously.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
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
Instances For
Returns the current array of InfoTrees and resets it to an empty array.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
This does the same job as realizeGlobalConstNoOverload
; 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
Instances For
Similar to realizeGlobalConstNoOverloadWithInfo
, except if there are multiple name resolutions then it returns them as a list.
Equations
Instances For
Adds a node containing the InfoTree
s generated by x
to the InfoTree
s in m
.
If x
succeeds and mkInfo
yields an Info
, the InfoTree
s of x
become subtrees of a node
containing the Info
produced by mkInfo
, which is then added to the InfoTree
s in m
.
If x
succeeds and mkInfo
yields an MVarId
, the InfoTree
s of x
are discarded and a hole
node is added to the InfoTree
s in m
.
If x
fails, the InfoTree
s of x
become subtrees of a node containing the Info
produced by
mkInfoOnError
, which is then added to the InfoTree
s in m
.
The InfoTree
s in m
are reset before x
is executed and restored with the addition of a new tree
after x
is executed.
Equations
Instances For
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
Instances For
Run x
as a new child infotree node with header given by mkInfo
.
Equations
Instances For
Resets the trees state t₀
, runs x
to produce a new trees state t₁
and sets the state to be
t₀ ++ (InfoTree.context (PartialContextInfo.commandCtx Γ) <$> t₁)
where Γ
is the context derived
from the monad state.
Equations
Instances For
Resets the trees state t₀
, runs x
to produce a new trees state t₁
and sets the state to be
t₀ ++ (InfoTree.context (PartialContextInfo.parentDeclCtx Γ) <$> t₁)
where Γ
is the parent decl
name provided by MonadParentDecl m
.