Add decidable equality function _≟_ to Haskell.Law.Eq.Def

agda · Jan 14, 2025 · 83a2ead · 83a2ead
1 parent 7cae101
commit 83a2ead
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/lib/Haskell/Law/Eq/Def.agda b/lib/Haskell/Law/Eq/Def.agda
@@ -7,6 +7,7 @@ open import Haskell.Prim.Double
 open import Haskell.Prim.Eq
 
 open import Haskell.Extra.Dec
+open import Haskell.Extra.Refinement
 
 open import Haskell.Law.Bool
 open import Haskell.Law.Equality
@@ -35,6 +36,12 @@ record IsLawfulEq (e : Set) ⦃ iEq : Eq e ⦄ : Set₁ where
 
 open IsLawfulEq ⦃ ... ⦄ public
 
+-- Types with a lawful Eq instance have decidable equality
+_≟_ : {{_ : Eq a}} {{_ : IsLawfulEq a}} → (x y : a) → Dec (x ≡ y)
+x ≟ y = (x == y) ⟨ isEquality x y ⟩
+
+{-# COMPILE AGDA2HS _≟_ inline #-}
+
 -- Reflexivity: x == x = True
 eqReflexivity : ⦃ iEq : Eq e ⦄ → ⦃ IsLawfulEq e ⦄
               → ∀ (x : e) → (x == x) ≡ True