lawful order Word code cleanup

agda · Dec 25, 2024 · 19d2c0e · 19d2c0e
1 parent 866d212
commit 19d2c0e
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 7 deletions.
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
@@ -3,8 +3,6 @@ module Haskell.Law.Ord.Def where
 open import Haskell.Prim
 open import Haskell.Prim.Ord
 open import Haskell.Prim.Bool
-open import Haskell.Prim.Word
-open import Haskell.Prim.Integer
 open import Haskell.Prim.Double
 open import Haskell.Prim.Tuple
 open import Haskell.Prim.Monoid
@@ -178,8 +176,6 @@ reverseLte a b c d
 
 postulate instance
 
-  -- iLawfulOrdWord : IsLawfulOrd Word
-
   iLawfulOrdDouble : IsLawfulOrd Double
 
   iLawfulOrdChar : IsLawfulOrd Char

diff --git a/lib/Haskell/Law/Ord/Word.agda b/lib/Haskell/Law/Ord/Word.agda
@@ -1,15 +1,12 @@
 module Haskell.Law.Ord.Word where
 
 open import Haskell.Prim
-open import Haskell.Prim.Bool
 open import Haskell.Prim.Eq
 open import Haskell.Prim.Ord
 open import Haskell.Prim.Word   using ( Word )
 
 open import Haskell.Law.Bool
-open import Haskell.Law.Equality
 open import Haskell.Law.Eq
-open import Haskell.Law.Eq.Instances
 open import Haskell.Law.Ord.Def
 open import Haskell.Law.Ord.Nat