Apply review suggestions

Co-authored by: Orestis Melkonian <melkon.or@gmail.com>

Author: HeinrichApfelmus

lib/containers/agda/Data/Map/Maybe.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --erasure #-}
 
 module Data.Map.Maybe
     {-

lib/containers/agda/Data/Map/Prop.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --erasure #-}
 
 -- | Proofs on 'Map'.
 module Data.Map.Prop where
@@ -14,13 +13,14 @@ open import Haskell.Data.Maybe using
 
 import Data.Map.Maybe as Maybe
 import Haskell.Prelude as List using (map)
+open import Data.Set using (Set)
 import Data.Set as Set
 
 {-----------------------------------------------------------------------------
     Proofs
     involving 1 value type
 ------------------------------------------------------------------------------}
-module _ {k a : Set} {{_ : Ord k}} where
+module _ {k a : Type} {{_ : Ord k}} where
 
   --
   prop-member-null
@@ -210,7 +210,7 @@ module _ {k a : Set} {{_ : Ord k}} where
     Proofs
     involving keysSet
 ------------------------------------------------------------------------------}
-module _ {k a : Set} {{_ : Ord k}} where
+module _ {k a : Type} {{_ : Ord k}} where
 
   --
   prop-member-keysSet
@@ -355,11 +355,11 @@ module _ {k a : Set} {{_ : Ord k}} where
     Proofs
     involving withoutKeys and restrictKeys
 ------------------------------------------------------------------------------}
-module _ {k a : Set} {{_ : Ord k}} where
+module _ {k a : Type} {{_ : Ord k}} where
 
   --
   prop-lookup-withoutKeys
-    : ∀ (key : k) (m : Map k a) (ks : Set.ℙ k)
+    : ∀ (key : k) (m : Map k a) (ks : Set k)
     → lookup key (withoutKeys m ks)
       ≡ Maybe.filt (not (Set.member key ks)) (lookup key m)
   --
@@ -377,7 +377,7 @@ module _ {k a : Set} {{_ : Ord k}} where
 
   --
   prop-lookup-restrictKeys
-    : ∀ (key : k) (m : Map k a) (ks : Set.ℙ k)
+    : ∀ (key : k) (m : Map k a) (ks : Set k)
     → lookup key (restrictKeys m ks)
       ≡ Maybe.filt (Set.member key ks) (lookup key m)
   --
@@ -441,7 +441,7 @@ module _ {k a : Set} {{_ : Ord k}} where
 
   --
   prop-restrictKeys-union
-    : ∀ (ma mb : Map k a) (ks : Set.ℙ k)
+    : ∀ (ma mb : Map k a) (ks : Set k)
     → restrictKeys (union ma mb) ks
       ≡ union (restrictKeys ma ks) (restrictKeys mb ks)
   --
@@ -499,7 +499,7 @@ module _ {k a : Set} {{_ : Ord k}} where
 
   --
   prop-withoutKeys-union
-    : ∀ (ma mb : Map k a) (ks : Set.ℙ k)
+    : ∀ (ma mb : Map k a) (ks : Set k)
     → withoutKeys (union ma mb) ks
       ≡ union (withoutKeys ma ks) (withoutKeys mb ks)
   --
@@ -531,7 +531,7 @@ module _ {k a : Set} {{_ : Ord k}} where
 
   --
   prop-withoutKeys-difference
-    : ∀ (m : Map k a) (ka kb : Set.ℙ k)
+    : ∀ (m : Map k a) (ka kb : Set k)
     → withoutKeys m (Set.difference ka kb)
       ≡ union (withoutKeys m ka) (restrictKeys m kb)
   --
@@ -582,7 +582,7 @@ module _ {k a : Set} {{_ : Ord k}} where
 
   --
   prop-withoutKeys-withoutKeys
-    : ∀ (m : Map k a) (ka kb : Set.ℙ k)
+    : ∀ (m : Map k a) (ka kb : Set k)
     → withoutKeys (withoutKeys m ka) kb
       ≡ withoutKeys m (Set.union ka kb)
   --
@@ -625,7 +625,7 @@ module _ {k a : Set} {{_ : Ord k}} where
 
   --
   @0 prop-withoutKeys-intersection
-    : ∀ (m : Map k a) (ka kb : Set.ℙ k)
+    : ∀ (m : Map k a) (ka kb : Set k)
     → withoutKeys m (Set.intersection ka kb)
       ≡ union (withoutKeys m ka) (withoutKeys m kb)
   --

lib/containers/agda/Data/Set/Prop.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --erasure #-}
 
 -- | Proofs on 'Set'.
 module Data.Set.Prop where
@@ -13,7 +12,7 @@ open import Haskell.Data.Set
     Properties
     Basic
 ------------------------------------------------------------------------------}
-module _ {a : Set} {{_ : Ord a}} where
+module _ {a : Type} {{_ : Ord a}} where
 
   --
   prop-null-empty
@@ -26,11 +25,11 @@ module _ {a : Set} {{_ : Ord a}} where
     Properties
     https://en.wikipedia.org/wiki/Boolean_algebra_(structure)
 ------------------------------------------------------------------------------}
-module _ {a : Set} {{_ : Ord a}} where
+module _ {a : Type} {{_ : Ord a}} where
 
   --
   prop-union-idem
-    : ∀ {sa : ℙ a}
+    : ∀ {sa : Set a}
     → union sa sa
         ≡ sa
   --
@@ -46,7 +45,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-union-assoc
-    : ∀ {sa sb sc : ℙ a}
+    : ∀ {sa sb sc : Set a}
     → union (union sa sb) sc
       ≡ union sa (union sb sc)
   --
@@ -66,7 +65,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-union-sym
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → union sa sb
         ≡ union sb sa
   --
@@ -83,7 +82,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-union-absorb
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → union sa (intersection sa sb)
       ≡ sa
   --
@@ -100,7 +99,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-union-identity
-    : ∀ {sa : ℙ a}
+    : ∀ {sa : Set a}
     → union sa empty
       ≡ sa
   --
@@ -117,7 +116,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-union-intersection-distribute
-    : ∀ {sa sb sc : ℙ a}
+    : ∀ {sa sb sc : Set a}
     → union sa (intersection sb sc)
       ≡ intersection (union sa sb) (union sa sc)
   --
@@ -139,7 +138,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-intersection-idem
-    : ∀ {sa : ℙ a}
+    : ∀ {sa : Set a}
     → intersection sa sa
         ≡ sa
   --
@@ -155,7 +154,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-intersection-assoc
-    : ∀ {sa sb sc : ℙ a}
+    : ∀ {sa sb sc : Set a}
     → intersection (intersection sa sb) sc
       ≡ intersection sa (intersection sb sc)
   --
@@ -175,7 +174,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-intersection-sym
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → intersection sa sb
         ≡ intersection sb sa
   --
@@ -192,7 +191,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-intersection-absorb
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → intersection sa (union sa sb)
       ≡ sa
   --
@@ -209,7 +208,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-intersection-union-distribute
-    : ∀ {sa sb sc : ℙ a}
+    : ∀ {sa sb sc : Set a}
     → intersection sa (union sb sc)
       ≡ union (intersection sa sb) (intersection sa sc)
   --
@@ -230,7 +229,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-intersection-empty-right
-    : ∀ {sa : ℙ a}
+    : ∀ {sa : Set a}
     → intersection sa empty
       ≡ empty
   --
@@ -247,7 +246,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-intersection-empty-left
-    : ∀ {sa : ℙ a}
+    : ∀ {sa : Set a}
     → intersection empty sa
       ≡ empty
   --
@@ -265,11 +264,11 @@ module _ {a : Set} {{_ : Ord a}} where
     Properties
     involving  difference
 ------------------------------------------------------------------------------}
-module _ {a : Set} {{_ : Ord a}} where
+module _ {a : Type} {{_ : Ord a}} where
 
   --
   prop-intersection-difference
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → intersection sb (difference sa sb)
       ≡ empty
   --
@@ -291,7 +290,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-disjoint-difference
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → disjoint sb (difference sa sb)
       ≡ True
   --
@@ -300,7 +299,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-union-difference
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → union (difference sa sb) sb
       ≡ union sa sb
   --
@@ -323,7 +322,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-difference-union-x
-    : ∀ {sa sb sc : ℙ a}
+    : ∀ {sa sb sc : Set a}
     → difference (union sa sb) sc
       ≡ union (difference sa sc) (difference sb sc)
   --
@@ -347,7 +346,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-deMorgan-difference-intersection
-    : ∀ {sa sb sc : ℙ a}
+    : ∀ {sa sb sc : Set a}
     → difference sa (intersection sb sc)
       ≡ union (difference sa sb) (difference sa sc)
   --
@@ -369,7 +368,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-deMorgan-difference-union
-    : ∀ {sa sb sc : ℙ a}
+    : ∀ {sa sb sc : Set a}
     → difference sa (union sb sc)
       ≡ intersection (difference sa sb) (difference sa sc)
   --
@@ -393,27 +392,27 @@ module _ {a : Set} {{_ : Ord a}} where
     Properties
     involving  isSubsetOf
 ------------------------------------------------------------------------------}
-module _ {a : Set} {{_ : Ord a}} where
+module _ {a : Type} {{_ : Ord a}} where
 
   -- | The 'empty' set is a subset of every set.
   prop-isSubsetOf-empty
-    : ∀ {sa : ℙ a}
+    : ∀ {sa : Set a}
     → isSubsetOf empty sa ≡ True
   --
   prop-isSubsetOf-empty {sa} =
     prop-intersection→isSubsetOf empty sa prop-intersection-empty-left
 
   -- | 'isSubsetOf' is reflexive
   prop-isSubsetOf-refl
-    : ∀ {sa : ℙ a}
+    : ∀ {sa : Set a}
     → isSubsetOf sa sa ≡ True
   --
   prop-isSubsetOf-refl {sa} =
     prop-intersection→isSubsetOf sa sa prop-intersection-idem
 
   -- | 'isSubsetOf' is antisymmetric
   prop-isSubsetOf-antisym
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → isSubsetOf sa sb ≡ True
     → isSubsetOf sb sa ≡ True
     → sa ≡ sb
@@ -440,7 +439,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   -- | 'isSubsetOf' is transitive
   prop-isSubsetOf-trans
-    : ∀ {sa sb sc : ℙ a}
+    : ∀ {sa sb sc : Set a}
     → isSubsetOf sa sb ≡ True
     → isSubsetOf sb sc ≡ True
     → isSubsetOf sa sc ≡ True
@@ -471,7 +470,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-isSubsetOf-intersection
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → isSubsetOf (intersection sa sb) sb ≡ True
   --
   prop-isSubsetOf-intersection {sa} {sb} =
@@ -487,7 +486,7 @@ module _ {a : Set} {{_ : Ord a}} where
 
   --
   prop-isSubsetOf-difference
-    : ∀ {sa sb : ℙ a}
+    : ∀ {sa sb : Set a}
     → isSubsetOf (difference sa sb) sa ≡ True
   --
   prop-isSubsetOf-difference {sa} {sb} =