def Lean.Elab.PartialContextInfo.mergeIntoOuter? (inner : PartialContextInfo) (outer? : Option ContextInfo) : Option ContextInfo

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.

def Lean.Elab.CompletionInfo.stx : CompletionInfo → Syntax

def Lean.Elab.CompletionInfo.lctx : CompletionInfo → LocalContext

Obtains the LocalContext from this CompletionInfo if available and yields an empty context otherwise.

partial def Lean.Elab.InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info

partial def Lean.Elab.InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMap MVarId InfoTree) : InfoTree

Instantiate the holes on the given tree with the assignment table. (analogous to instantiating the metavariables in an expression)

def Lean.Elab.InfoState.substituteLazy (s : InfoState) : Task InfoState

Applies s.lazyAssignment to s.trees, asynchronously.

structure Lean.Elab.LinterInfoGroup : Type

@[instance_reducible]

instance Lean.Elab.instTypeNameLinterInfoGroup : TypeName LinterInfoGroup

def Lean.Elab.mkLinterInfoGroupNode (trees : PersistentArray InfoTree) : InfoTree

def Lean.Elab.pushInfoChild : InfoTree → InfoTree → InfoTree

def Lean.Elab.Info.toElabInfo? : Info → Option ElabInfo

def Lean.Elab.Info.updateContext? : Option ContextInfo → Info → Option ContextInfo

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.

def Lean.Elab.Info.stx : Info → Syntax

partial def Lean.Elab.InfoTree.addTrailing? (trailing : Substring.Raw) : InfoTree → Option InfoTree

Adds the given trailing substring to all adjacent syntax in the info tree if any, otherwise returns none.

def Lean.Elab.InfoTree.addTrailing (trailing : Substring.Raw) (t : InfoTree) : InfoTree

Adds the given trailing substring to all adjacent syntax in the info tree.