Documentation

Lean.Elab.InfoTree.Basic

source
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.

Equations
Instances For
    source
    def Lean.Elab.CompletionInfo.stx :
    CompletionInfo → Syntax
    Equations
    Instances For
      source
      def Lean.Elab.CompletionInfo.lctx :
      CompletionInfo → LocalContext

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

      Equations
      Instances For
        source
        partial def Lean.Elab.InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) :
        Option Info
        source
        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)

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

        Applies s.lazyAssignment to s.trees, asynchronously.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.Info.toElabInfo? :
          Info → Option ElabInfo
          Equations
          Instances For
            source
            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.

            Equations
            Instances For
              source
              def Lean.Elab.Info.stx :
              Info → Syntax
              Equations
              Instances For
                source
                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.

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

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

                Equations
                Instances For