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

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

Equations

• (Lean.Meta.DiscrTree.Key.lit v₁).cmp (Lean.Meta.DiscrTree.Key.lit v₂) = compare v₁ v₂
• (Lean.Meta.DiscrTree.Key.fvar n₁ a₁).cmp (Lean.Meta.DiscrTree.Key.fvar n₂ a₂) = (n₁.name.quickCmp n₂.name).then (compare a₁ a₂)
• (Lean.Meta.DiscrTree.Key.const n₁ a₁).cmp (Lean.Meta.DiscrTree.Key.const n₂ a₂) = (n₁.quickCmp n₂).then (compare a₁ a₂)
• (Lean.Meta.DiscrTree.Key.proj s₁ i₁ a₁).cmp (Lean.Meta.DiscrTree.Key.proj s₂ i₂ a₂) = (s₁.quickCmp s₂).then ((compare i₁ i₂).then (compare a₁ a₂))
• x✝¹.cmp x✝ = compare x✝¹.ctorIdx x✝.ctorIdx

@[implicit_reducible]

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

Equations

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

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.

Equations

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