Documentation

Mathlib.Lean.Elab.InfoTree

Additions to Lean.Elab.InfoTree.Main #

source
def Lean.Elab.collectTryThisSuggestions (trees : PersistentArray InfoTree) :
Array Meta.Tactic.TryThis.Suggestion

Collects all suggestions from all TryThisInfos in trees. trees is visited in order and suggestions in each tree are collected in post-order.

Equations
Instances For
    source
    def Lean.Elab.collectTryThisSuggestions.go (trees : PersistentArray InfoTree) :
    StateM (Array Meta.Tactic.TryThis.Suggestion) Unit

    Visits all trees.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.collectTryThisSuggestions.visitNode (_ctx : ContextInfo) (i : Info) (_children : PersistentArray InfoTree) :
      StateM (Array Meta.Tactic.TryThis.Suggestion) Unit

      Visits a node in a tree.

      Equations
      Instances For