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.

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

Equations

• Lean.Meta.DiscrTree.Key.instOrd_batteries = { compare := Lean.Meta.DiscrTree.Key.cmp }

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.

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.

@[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.