remove unused imports

agda · Dec 23, 2023 · ae8e914 · ae8e914
1 parent a1c57da
commit ae8e914
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 6 deletions.
diff --git a/lib/Haskell/Law/List.agda b/lib/Haskell/Law/List.agda
@@ -98,6 +98,14 @@ lengthNat-++ (x ∷ xs) = cong suc (lengthNat-++ xs)
 ∷-not-identity : ∀ x (xs ys : List a) → (x ∷ xs) ++ ys ≡ ys → ⊥
 ∷-not-identity x xs ys eq = []≠∷ x xs (sym $ ++-identity-left-unique (x ∷ xs) (sym eq))
 
+concatMap-++-distr : ∀ (xs ys : List a) (f : a → List b ) → 
+  ((concatMap f xs) ++ (concatMap f ys)) ≡ (concatMap f (xs ++ ys))
+concatMap-++-distr [] ys f = refl
+concatMap-++-distr (x ∷ xs) ys f
+  rewrite ++-assoc (f x) (concatMap f xs) (concatMap f ys)
+  | concatMap-++-distr xs ys f
+ = refl
+
 --------------------------------------------------
 -- foldr
 

diff --git a/lib/Haskell/Law/Monad/List.agda b/lib/Haskell/Law/Monad/List.agda
@@ -3,7 +3,6 @@ module Haskell.Law.Monad.List where
 open import Haskell.Prim
 open import Haskell.Prim.Foldable
 open import Haskell.Prim.List
-open import Haskell.Prim.Monoid
 
 open import Haskell.Prim.Monad
 
@@ -39,7 +38,7 @@ instance
     = refl
   iLawfulMonadList .associativity (x ∷ xs) f g
     rewrite associativity xs f g
-    | concatMap-distr (f x) (concatMap f xs) g
+    | concatMap-++-distr (f x) (concatMap f xs) g
     = refl  
 
   iLawfulMonadList .pureIsReturn _ = refl

diff --git a/lib/Haskell/Law/Monoid/List.agda b/lib/Haskell/Law/Monoid/List.agda
@@ -1,12 +1,10 @@
 module Haskell.Law.Monoid.List where
 
 open import Haskell.Prim
-open import Haskell.Prim.Foldable
 open import Haskell.Prim.List
 
 open import Haskell.Prim.Monoid
 
-open import Haskell.Law.Equality
 open import Haskell.Law.List
 open import Haskell.Law.Monoid.Def
 open import Haskell.Law.Semigroup.Def

diff --git a/lib/Haskell/Law/Monoid/Maybe.agda b/lib/Haskell/Law/Monoid/Maybe.agda
@@ -1,12 +1,10 @@
 module Haskell.Law.Monoid.Maybe where
 
 open import Haskell.Prim
-open import Haskell.Prim.Foldable
 open import Haskell.Prim.Maybe
 
 open import Haskell.Prim.Monoid
 
-open import Haskell.Law.Equality
 open import Haskell.Law.Monoid.Def
 open import Haskell.Law.Semigroup.Def
 open import Haskell.Law.Semigroup.Maybe