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

jespercockx · Dec 19, 2023 · 6c866c9 · 6c866c9
1 parent e599846
commit 6c866c9
Show file tree

Hide file tree

Showing 2 changed files with 1 addition 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)