Decidable equivalence for TreeMap

@[implicit_reducible]

instance Std.TreeMap.instDecidableEquivOfTransCmpOfLawfulEqCmpOfLawfulBEq {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : TreeMap α β cmp} : Decidable (t₁.Equiv t₂)

Equations

• Std.TreeMap.instDecidableEquivOfTransCmpOfLawfulEqCmpOfLawfulBEq = decidable_of_iff (t₁.inner.Equiv t₂.inner) ⋯