Remove re-export of Haskell.Law modules from Haskell.Prelude

viktorcsimma · Dec 27, 2023 · 9a7b90b · 9a7b90b
1 parent b46b901
commit 9a7b90b
Showing 5 changed files with 7 additions and 13 deletions.
diff --git a/lib/Haskell/Extra/Dec.agda b/lib/Haskell/Extra/Dec.agda
@@ -1,6 +1,6 @@
 module Haskell.Extra.Dec where
 
-open import Haskell.Prelude hiding (Reflects)
+open import Haskell.Prelude
 open import Haskell.Extra.Refinement
 open import Agda.Primitive
 

diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
@@ -39,18 +39,6 @@ open import Haskell.Prim.Traversable public
 open import Haskell.Prim.Tuple       public hiding (first; second; _***_)
 open import Haskell.Prim.Word        public
 
-open import Haskell.Law              public
-open import Haskell.Law.Applicative  public
-open import Haskell.Law.Bool         public
-open import Haskell.Law.Eq           public
-open import Haskell.Law.Equality     public
-open import Haskell.Law.Functor      public
-open import Haskell.Law.List         public
-open import Haskell.Law.Maybe        public
-open import Haskell.Law.Monad        public
-open import Haskell.Law.Monoid       public
-open import Haskell.Law.Ord          public
-
 -- Problematic features
 --  - [Partial]:  Could pass implicit/instance arguments to prove totality.
 --  - [Float]:    Or Float (Agda floats are Doubles)

diff --git a/test/HeightMirror.agda b/test/HeightMirror.agda
@@ -1,5 +1,6 @@
 
 open import Haskell.Prelude hiding (max)
+open import Haskell.Law.Equality
 
 subst : {p : @0 a → Set} {@0 m n : a} → @0 m ≡ n → p m → p n
 subst refl t = t

diff --git a/test/LawfulOrd.agda b/test/LawfulOrd.agda
@@ -1,4 +1,5 @@
 open import Haskell.Prelude
+open import Haskell.Law
 
 data Ordered (a : Set) : Set where
     Gt : ⦃ @0 iOrd : Ord a ⦄ → (a' : a) → (a'' : a) → ⦃ @0 pf : (a' > a'') ≡ True ⦄ → Ordered a

diff --git a/test/golden/Haskell/Extra/Dec.hs b/test/golden/Haskell/Extra/Dec.hs
@@ -0,0 +1,4 @@
+module Haskell.Extra.Dec where
+
+type Dec = Bool
+
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,4 @@
		module Haskell.Extra.Dec where

		type Dec = Bool