Decidable equivalence for DTreeMap.Raw

@[implicit_reducible]

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

Equations

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