From 83a2ead1aba26b76b8b0122063740f4313e45525 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 14 Jan 2025 17:32:00 +0100
Subject: [PATCH] =?UTF-8?q?Add=20decidable=20equality=20function=20`=5F?=
 =?UTF-8?q?=E2=89=9F=5F`=20to=20`Haskell.Law.Eq.Def`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lib/Haskell/Law/Eq/Def.agda | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/lib/Haskell/Law/Eq/Def.agda b/lib/Haskell/Law/Eq/Def.agda
index 957da9f1..0d519207 100644
--- 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