Final Data.Product import simplifications (#2052)

Author: Saransh-cpp

README/Case.agda

@@ -12,7 +12,6 @@ module README.Case where
 open import Data.Fin   hiding (pred)
 open import Data.Maybe hiding (from-just)
 open import Data.Nat   hiding (pred)
-open import Data.Product
 open import Function.Base using (case_of_; case_return_of_)
 open import Relation.Nullary
 open import Relation.Binary

README/Data/Container/Indexed.agda

@@ -11,7 +11,7 @@ module README.Data.Container.Indexed where
 open import Data.Unit
 open import Data.Empty
 open import Data.Nat.Base
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_)
 open import Data.W.Indexed
 open import Data.Container.Indexed

README/Data/Integer.agda

@@ -51,7 +51,6 @@ ex₅ i j = ℤₚ.*-comm i j
 -- provides some combinators for equational reasoning.
 
 open P.≡-Reasoning
-open import Data.Product
 
 ex₆ : ∀ i j → i * (j + + 0) ≡ j * i
 ex₆ i j = begin

README/Data/List/Fresh.agda

@@ -12,7 +12,7 @@ open import Data.Nat
 open import Data.List.Base
 open import Data.List.Fresh
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
-open import Data.Product
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Relation.Nary using (⌊_⌋; fromWitness)
 
 -- A sorted list of natural numbers can be seen as a fresh list

README/Data/Record.agda

@@ -11,7 +11,7 @@
 
 module README.Data.Record where
 
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.String
 open import Function.Base using (flip)
 open import Level

README/Data/Trie/NonDependent.agda

@@ -56,7 +56,7 @@ import Data.Char.Properties  as Char
 open import Data.List.Base   as List using (List; []; _∷_)
 open import Data.List.Fresh  as List# using (List#; []; _∷#_)
 open import Data.Maybe       as Maybe
-open import Data.Product     as Prod
+open import Data.Product.Base as Prod using (_×_; ∃; proj₁; _,_)
 open import Data.String.Base as String using (String)
 open import Data.String.Properties as String using (_≟_)
 open import Data.These       as These

README/Data/Wrap.agda

@@ -13,7 +13,7 @@ open import Data.Wrap
 open import Algebra
 open import Data.Nat
 open import Data.Nat.Properties
-open import Data.Product
+open import Data.Product.Base using (_,_; ∃; ∃₂; _×_)
 open import Level using (Level)
 open import Relation.Binary
 

README/Design/Decidability.agda

@@ -13,7 +13,7 @@ open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Properties using (∷-injective)
 open import Data.Nat
 open import Data.Nat.Properties using (suc-injective)
-open import Data.Product
+open import Data.Product.Base using (uncurry)
 open import Data.Unit
 open import Function.Base using (id;  _∘_)
 open import Relation.Binary.PropositionalEquality

README/Foreign/Haskell.agda

@@ -22,7 +22,7 @@ open import Data.Bool.Base using (Bool; if_then_else_)
 open import Data.Char as Char
 open import Data.List.Base as List using (List; _∷_; []; takeWhile; dropWhile)
 open import Data.Maybe.Base using (Maybe; just; nothing)
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Function
 open import Relation.Nullary.Decidable
 

README/Inspect.agda

@@ -14,7 +14,7 @@ module README.Inspect where
 
 open import Data.Nat.Base
 open import Data.Nat.Properties
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Binary.PropositionalEquality using (inspect)