Decidable equivalence for TreeSet

@[implicit_reducible]

instance Std.TreeSet.instDecidableEquivOfTransCmpOfLawfulEqCmp {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : TreeSet α cmp} : Decidable (t₁.Equiv t₂)

Equations

• Std.TreeSet.instDecidableEquivOfTransCmpOfLawfulEqCmp = decidable_of_iff (t₁.inner.Equiv t₂.inner) ⋯