Decidable equivalence for TreeSet.Raw

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

Equations

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