Decidable equivalence for HashSet.Raw

instance Std.HashSet.Raw.instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁.Equiv m₂)

Equations

• Std.HashSet.Raw.instDecidableEquiv h₁ h₂ = decidable_of_iff (m₁.inner.Equiv m₂.inner) ⋯