[ fix #302 ] Move _/=_ function out of the Eq record

agda · May 24, 2024 · f17b86c · f17b86c
1 parent 4e66970
commit f17b86c
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 4 deletions.
diff --git a/lib/Haskell/Prim/Eq.agda b/lib/Haskell/Prim/Eq.agda
@@ -16,17 +16,19 @@ open import Haskell.Prim.Either
 -- Eq
 
 record Eq (a : Set) : Set where
-  infix 4 _==_ _/=_
+  infix 4 _==_
   field
     _==_ : a → a → Bool
 
-  _/=_ : a → a → Bool
-  x /= y = not (x == y)
-
 open Eq ⦃...⦄ public
 
 {-# COMPILE AGDA2HS Eq existing-class #-}
 
+_/=_ : {{Eq a}} → a → a → Bool
+x /= y = not (x == y)
+
+infix 4 _/=_
+
 instance
   iEqNat : Eq Nat
   iEqNat ._==_ = eqNat

diff --git a/test/AllTests.agda b/test/AllTests.agda
@@ -82,6 +82,7 @@ import Issue145
 import Issue264
 import Issue301
 import Issue305
+import Issue302
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -161,4 +162,5 @@ import Issue145
 import Issue264
 import Issue301
 import Issue305
+import Issue302
 #-}
diff --git a/test/Issue302.agda b/test/Issue302.agda
@@ -0,0 +1,5 @@
+open import Haskell.Prelude
+
+not0 : Int → Bool
+not0 n = n /= 0
+{-# COMPILE AGDA2HS not0 #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
@@ -77,4 +77,5 @@ import Issue145
 import Issue264
 import Issue301
 import Issue305
+import Issue302
 
diff --git a/test/golden/Issue302.hs b/test/golden/Issue302.hs
@@ -0,0 +1,5 @@
+module Issue302 where
+
+not0 :: Int -> Bool
+not0 n = n /= 0
+