Leftover Data.List simplifications

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.List
 open import Data.Product
 open import Function.Base using (case_of_; case_return_of_)
 open import Relation.Nullary

README/Design/Decidability.agda

@@ -9,7 +9,7 @@
 module README.Design.Decidability where
 
 open import Data.Bool
-open import Data.List
+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)

src/Data/List/Relation/Unary/Enumerates/Setoid.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.List
+open import Data.List.Base using (List)
 open import Level
 open import Relation.Binary
 

src/Data/List/Relation/Unary/Grouped/Properties.agda

@@ -9,7 +9,7 @@
 module Data.List.Relation.Unary.Grouped.Properties where
 
 open import Data.Bool using (true; false)
-open import Data.List
+open import Data.List.Base using ([]; [_]; _∷_; map; derun)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)

src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.List
+open import Data.List.Base using ([]; _∷_; deduplicate)
 import Data.List.Relation.Unary.Unique.DecSetoid as Unique
 open import Data.List.Relation.Unary.All.Properties using (all-filter)
 open import Data.List.Relation.Unary.Unique.Setoid.Properties