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
Without this function, the formatting method would often fail when processing
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
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.
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.
resolveGlobalConstNoOverloadWithInfo, except if there are multiple name resolutions then it returns them as a list.
resolveGlobalName, but it also adds the resolved name to the info tree.
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.
x >>= mkInfo will modify the trees state and produce a new list of trees
i : Info case,
t₁ become the children of a node
node i t₁ that is appended to
Saves the current list of trees
x to produce a new tree list
mkInfoTree t₁ to get
n : InfoTree and then restores the trees to be
t₀ ++ [n].
Resets the trees state
x to produce a new trees
t₁ and sets the state to be
t₀ ++ (InfoTree.context Γ <$> t₁)
Γ is the context derived from the monad state.