Documentation

Std.Lean.Meta.DiscrTree

source
def Lean.Meta.DiscrTree.Key.cmp :
Lean.Meta.DiscrTree.Key → Lean.Meta.DiscrTree.Key → Ordering

Compare two Keys. The ordering is total but otherwise arbitrary. (It uses Name.quickCmp internally.)

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance Lean.Meta.DiscrTree.Key.instOrdKey :
    Ord Lean.Meta.DiscrTree.Key
    Equations
    source
    partial def Lean.Meta.DiscrTree.Trie.mergePreservingDuplicates {α : Type} :
    Lean.Meta.DiscrTree.Trie α → Lean.Meta.DiscrTree.Trie α → Lean.Meta.DiscrTree.Trie α

    Merge two Tries. Duplicate values are preserved.

    source
    partial def Lean.Meta.DiscrTree.Trie.mergePreservingDuplicates.mergeChildren {α : Type} (cs₁ : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) (cs₂ : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) :
    Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)

    Auxiliary definition for mergePreservingDuplicates.

    source
    @[inline]
    def Lean.Meta.DiscrTree.mergePreservingDuplicates {α : Type} (t : Lean.Meta.DiscrTree α) (u : Lean.Meta.DiscrTree α) :
    Lean.Meta.DiscrTree α

    Merge two DiscrTrees. Duplicate values are preserved.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For