diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda index 57350348..ab153c54 100644 --- 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 index d961a4eb..3b007c81 100644 --- 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