Decidable equivalence for DHashMap.Raw

instance Std.DHashMap.Raw.instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [(k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁.Equiv m₂)

Equations

• Std.DHashMap.Raw.instDecidableEquiv h₁ h₂ = Std.DHashMap.Internal.Raw₀.decidableEquiv ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩ h₁ h₂