Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
- (Lean.Elab.PartialContextInfo.commandCtx info).mergeIntoOuter? none = some { toCommandContextInfo := info, parentDecl? := none }
- (Lean.Elab.PartialContextInfo.commandCtx innerInfo).mergeIntoOuter? (some outer) = some { toCommandContextInfo := innerInfo, parentDecl? := outer.parentDecl? }
- (Lean.Elab.PartialContextInfo.parentDeclCtx innerParentDecl).mergeIntoOuter? (some outer) = some { toCommandContextInfo := outer.toCommandContextInfo, parentDecl? := some innerParentDecl }
Instances For
Equations
- (Lean.Elab.CompletionInfo.dot i expectedType?).stx = i.stx
- (Lean.Elab.CompletionInfo.id stx id danglingDot lctx expectedType?).stx = stx
- (Lean.Elab.CompletionInfo.dotId stx id lctx expectedType?).stx = stx
- (Lean.Elab.CompletionInfo.fieldId stx id lctx structName).stx = stx
- (Lean.Elab.CompletionInfo.namespaceId stx).stx = stx
- (Lean.Elab.CompletionInfo.option stx).stx = stx
- (Lean.Elab.CompletionInfo.endSection stx scopeNames).stx = stx
- (Lean.Elab.CompletionInfo.tactic stx).stx = stx
Instances For
Obtains the LocalContext
from this CompletionInfo
if available and yields an empty context
otherwise.
Equations
- (Lean.Elab.CompletionInfo.dot i expectedType?).lctx = i.lctx
- (Lean.Elab.CompletionInfo.id stx id danglingDot lctx expectedType?).lctx = lctx
- (Lean.Elab.CompletionInfo.dotId stx id lctx expectedType?).lctx = lctx
- (Lean.Elab.CompletionInfo.fieldId stx id lctx structName).lctx = lctx
- x.lctx = Lean.LocalContext.empty
Instances For
Equations
- x.format = Lean.format "CustomInfo(" ++ Lean.format x.value.typeName ++ Lean.format ")"
Instances For
Equations
- Lean.Elab.instToFormatCustomInfo = { format := Lean.Elab.CustomInfo.format }
Instantiate the holes on the given tree
with the assignment table.
(analogous to instantiating the metavariables in an expression)
Embeds a CoreM
action in IO
by supplying the information stored in info
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- info.toPPContext lctx = { env := info.env, mctx := info.mctx, lctx := lctx, opts := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls }
Instances For
Equations
- info.ppSyntax lctx stx = Lean.ppTerm (info.toPPContext lctx) { raw := stx }
Instances For
Equations
- info.runMetaM ctx x = ctx.runMetaM info.lctx x
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.CommandInfo.format ctx info = pure (Lean.format "command @ " ++ Lean.format (Lean.Elab.formatElabInfo ctx info.toElabInfo) ++ Lean.format "")
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.FieldRedeclInfo.format ctx info = Lean.format "FieldRedecl @ " ++ Lean.format (Lean.Elab.formatStxRange ctx info.stx) ++ Lean.format ""
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofTacticInfo i) = Lean.Elab.TacticInfo.format ctx i
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofTermInfo i) = Lean.Elab.TermInfo.format ctx i
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofCommandInfo i) = Lean.Elab.CommandInfo.format ctx i
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofMacroExpansionInfo i) = Lean.Elab.MacroExpansionInfo.format ctx i
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofOptionInfo i) = Lean.Elab.OptionInfo.format ctx i
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofFieldInfo i) = Lean.Elab.FieldInfo.format ctx i
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofCompletionInfo i) = Lean.Elab.CompletionInfo.format ctx i
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofUserWidgetInfo i) = pure i.format
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofCustomInfo i) = pure (Lean.format i)
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofFVarAliasInfo i) = pure i.format
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofFieldRedeclInfo i) = pure (Lean.Elab.FieldRedeclInfo.format ctx i)
- Lean.Elab.Info.format ctx (Lean.Elab.Info.ofOmissionInfo i) = Lean.Elab.OmissionInfo.format ctx i
Instances For
Equations
- (Lean.Elab.Info.ofTacticInfo i).toElabInfo? = some i.toElabInfo
- (Lean.Elab.Info.ofTermInfo i).toElabInfo? = some i.toElabInfo
- (Lean.Elab.Info.ofCommandInfo i).toElabInfo? = some i.toElabInfo
- (Lean.Elab.Info.ofMacroExpansionInfo i).toElabInfo? = none
- (Lean.Elab.Info.ofOptionInfo i).toElabInfo? = none
- (Lean.Elab.Info.ofFieldInfo i).toElabInfo? = none
- (Lean.Elab.Info.ofCompletionInfo i).toElabInfo? = none
- (Lean.Elab.Info.ofUserWidgetInfo i).toElabInfo? = none
- (Lean.Elab.Info.ofCustomInfo i).toElabInfo? = none
- (Lean.Elab.Info.ofFVarAliasInfo i).toElabInfo? = none
- (Lean.Elab.Info.ofFieldRedeclInfo i).toElabInfo? = none
- (Lean.Elab.Info.ofOmissionInfo i).toElabInfo? = some i.toElabInfo
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
- One or more equations did not get rendered due to their size.
- Lean.Elab.Info.updateContext? x✝ x = x✝
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Instances For
Similar to realizeGlobalConstNoOverloadWithInfo
, 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.
Instances For
Similar to realizeGlobalName
, but it also adds the resolved name to the info tree.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
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
- One or more equations did not get rendered due to their size.
Instances For
Run x
as a new child infotree node with header given by mkInfo
.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.getInfoHoleIdAssignment? mvarId = do let __do_lift ← Lean.Elab.getInfoState pure __do_lift.assignment[mvarId]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.enableInfoTree flag = Lean.Elab.modifyInfoState fun (s : Lean.Elab.InfoState) => { enabled := flag, assignment := s.assignment, trees := s.trees }
Instances For
Equations
- One or more equations did not get rendered due to their size.