Decidable equivalence for TreeMap.Raw

def Std.TreeMap.Raw.instDecidableEquiv {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁.Equiv t₂)

Equations

• Std.TreeMap.Raw.instDecidableEquiv h₁ h₂ = decidable_of_iff (t₁.inner.Equiv t₂.inner) ⋯