Documentation

Batteries.Lean.Meta.DiscrTree

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

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

Instances For
    source
    @[instance_reducible]
    instance Lean.Meta.DiscrTree.Key.instOrd_batteries :
    Ord Key
    source
    partial def Lean.Meta.DiscrTree.Trie.mergePreservingDuplicates {α : Type} (t₁ t₂ : Trie α) :
    Trie α

    Merge two Tries. Duplicate values are preserved.

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

    Merge two DiscrTrees. Duplicate values are preserved.

    Instances For