Decidable equivalence for DTreeMap

@[instance_reducible]

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

Equations

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