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

Compare two `Key`s. 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

Instances For

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

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

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

Merge two `Trie`s. Duplicate values are preserved.

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

Auxiliary definition for `mergePreservingDuplicates`.

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

Merge two `DiscrTree`s. Duplicate values are preserved.

Equations

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

Instances For