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

• (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

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₁ 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 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.