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

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

@[implicit_reducible]

instance Lean.Meta.DiscrTree.Key.instOrd_batteries : Ord Key

partial def Lean.Meta.DiscrTree.Trie.mergePreservingDuplicates {α : Type} : Trie α → Trie α → Trie α

Merge two Tries. Duplicate values are preserved.

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

Auxiliary definition for mergePreservingDuplicates.

@[inline]

def Lean.Meta.DiscrTree.mergePreservingDuplicates {α : Type} (t u : DiscrTree α) : DiscrTree α

Merge two DiscrTrees. Duplicate values are preserved.