diff --git a/lib/Haskell/Prim/Eq.agda b/lib/Haskell/Prim/Eq.agda index f8bcd23a..a710dbf8 100644 --- 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 index c1a58587..c0ceb099 100644 --- 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 new file mode 100644 index 00000000..215342ad --- /dev/null +++ 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 index 51ab5ba2..c1603dff 100644 --- 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 new file mode 100644 index 00000000..03305844 --- /dev/null +++ b/test/golden/Issue302.hs @@ -0,0 +1,5 @@ +module Issue302 where + +not0 :: Int -> Bool +not0 n = n /= 0 +