Simplify Data.List imports to Data.List.Base (#2007)

Saransh-cpp · plt-amy · commit b6322d33dc77 · 2023-07-21T13:07:42.000-03:00
diff --git a/README/Data/List/Relation/Binary/Pointwise.agda b/README/Data/List/Relation/Binary/Pointwise.agda
@@ -7,7 +7,7 @@
 module README.Data.List.Relation.Binary.Pointwise where
 
 open import Data.Nat using (ℕ; _<_; s≤s; z≤n)
-open import Data.List using (List; []; _∷_; length)
+open import Data.List.Base using (List; []; _∷_; length)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; setoid)
 open import Relation.Nullary.Negation using (¬_)
diff --git a/README/Data/List/Relation/Binary/Subset.agda b/README/Data/List/Relation/Binary/Subset.agda
@@ -4,7 +4,7 @@
 -- Documentation for subset relations over `List`s
 ------------------------------------------------------------------------
 
-open import Data.List using (List; _∷_; [])
+open import Data.List.Base using (List; _∷_; [])
 open import Data.List.Membership.Propositional.Properties
   using (∈-++⁺ˡ; ∈-insert)
 open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
diff --git a/README/Data/Tree/AVL.agda b/README/Data/Tree/AVL.agda
@@ -60,7 +60,7 @@ t₃ = delete 2 t₂
 
 -- Conversion of a list of key-value mappings to a tree.
 
-open import Data.List using (_∷_; [])
+open import Data.List.Base using (_∷_; [])
 
 t₄ : Tree
 t₄ = fromList ((2 , v₂) ∷ (1 , v₁) ∷ [])
diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda
@@ -53,7 +53,7 @@ open import Data.Unit
 open import Data.Bool
 open import Data.Char        as Char
 import Data.Char.Properties  as Char
-open import Data.List        as List using (List; []; _∷_)
+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
diff --git a/README/Tactic/RingSolver.agda b/README/Tactic/RingSolver.agda
@@ -28,7 +28,7 @@ instance
 ------------------------------------------------------------------------------
 -- Imports!
 
-open import Data.List as List using (List; _∷_; [])
+open import Data.List.Base as List using (List; _∷_; [])
 open import Function
 open import Relation.Binary.PropositionalEquality
   using (subst; cong; _≡_; module ≡-Reasoning)
diff --git a/README/Text/Regex.agda b/README/Text/Regex.agda
@@ -9,7 +9,7 @@
 module README.Text.Regex where
 
 open import Data.Bool using (true; false)
-open import Data.List using (_∷_; [])
+open import Data.List.Base using (_∷_; [])
 open import Data.String
 open import Function.Base using () renaming (_$′_ to _$_)
 open import Relation.Nullary.Decidable using (yes)
diff --git a/src/Data/Fin/Permutation/Transposition/List.agda b/src/Data/Fin/Permutation/Transposition/List.agda
@@ -12,7 +12,7 @@ open import Data.Fin.Base
 open import Data.Fin.Patterns using (0F)
 open import Data.Fin.Permutation as P hiding (lift₀)
 import Data.Fin.Permutation.Components as PC
-open import Data.List using (List; []; _∷_; map)
+open import Data.List.Base using (List; []; _∷_; map)
 open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Product using (_×_; _,_)
 open import Function.Base using (_∘_)
diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda
@@ -20,7 +20,7 @@ open import Function.Base
 open import Function.Bundles
   using (Injection; module Injection)
 open import Data.Bool.Base using (true; false)
-open import Data.List hiding (lookup)
+open import Data.List.Base hiding (lookup)
 open import Data.List.Relation.Unary.Any as Any using (here; there)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
@@ -24,7 +24,7 @@ open import Data.Maybe.Base as M
 open import Data.Nat.Base as Nat using (ℕ)
 open import Data.Product
 open import Data.Vec.Base as Vec using (Vec ; lookup)
-open import Data.List hiding (lookup)
+open import Data.List.Base hiding (lookup)
 open import Data.List.Properties
 open import Data.List.Relation.Binary.Sublist.Heterogeneous
   hiding (lookup)
diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
@@ -8,7 +8,7 @@
 
 module Data.List.Relation.Unary.AllPairs.Properties where
 
-open import Data.List hiding (any)
+open import Data.List.Base hiding (any)
 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; []; _∷_)
diff --git a/src/Data/List/Relation/Unary/Grouped.agda b/src/Data/List/Relation/Unary/Grouped.agda
@@ -8,7 +8,7 @@
 
 module Data.List.Relation.Unary.Grouped where
 
-open import Data.List using (List; []; _∷_; map)
+open import Data.List.Base using (List; []; _∷_; map)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_; all?)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_; _,_)
diff --git a/src/Data/Tree/Binary/Zipper.agda b/src/Data/Tree/Binary/Zipper.agda
@@ -10,7 +10,7 @@ module Data.Tree.Binary.Zipper where
 
 open import Level using (Level; _⊔_)
 open import Data.Tree.Binary as BT using (Tree; node; leaf)
-open import Data.List as List using (List; []; _∷_; sum; _++_; [_])
+open import Data.List.Base as List using (List; []; _∷_; sum; _++_; [_])
 open import Data.Maybe using (Maybe; nothing; just)
 open import Data.Nat.Base using (ℕ; suc; _+_)
 open import Function
diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
@@ -13,7 +13,7 @@ open import Data.Fin.Base
 open import Data.Nat as ℕ
 import Data.Nat.Properties as ℕₚ
 open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
-open import Data.List as L using (List)
+open import Data.List.Base as L using (List)
 import Data.List.Properties as Lₚ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.Vec as V using (Vec)
diff --git a/src/Data/Vec/Reflection.agda b/src/Data/Vec/Reflection.agda
@@ -8,7 +8,7 @@
 
 module Data.Vec.Reflection where
 
-import Data.List as List
+import Data.List.Base as List
 open import Data.Vec.Base
 open import Reflection.AST.Term
 open import Reflection.AST.Argument
diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda
@@ -13,7 +13,7 @@ module Reflection.AST.Show where
 
 import Data.Char as Char   using (show)
 import Data.Float as Float using (show)
-open import Data.List hiding (_++_; intersperse)
+open import Data.List.Base hiding (_++_; intersperse)
 import Data.Nat.Show as ℕ using (show)
 open import Data.Product   using (_×_; _,_)
 open import Data.String as String
diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda
@@ -12,7 +12,7 @@ module Reflection.AST.Traversal
   {F : Set → Set} (AppF : RawApplicative F) where
 
 open import Data.Nat          using (ℕ; zero; suc; _+_)
-open import Data.List         using (List; []; _∷_; _++_; reverse; length)
+open import Data.List.Base    using (List; []; _∷_; _++_; reverse; length)
 open import Data.Product      using (_×_; _,_)
 open import Data.String       using (String)
 open import Function.Base     using (_∘_)
diff --git a/src/Tactic/MonoidSolver.agda b/src/Tactic/MonoidSolver.agda
@@ -75,11 +75,11 @@ module Tactic.MonoidSolver where
 open import Algebra
 open import Function
 
-open import Data.Bool    as Bool    using (Bool; _∨_; if_then_else_)
-open import Data.Maybe   as Maybe   using (Maybe; just; nothing; maybe)
-open import Data.List    as List    using (List; _∷_; [])
-open import Data.Nat     as ℕ       using (ℕ; suc; zero)
-open import Data.Product as Product using (_×_; _,_)
+open import Data.Bool         as Bool    using (Bool; _∨_; if_then_else_)
+open import Data.Maybe        as Maybe   using (Maybe; just; nothing; maybe)
+open import Data.List.Base    as List    using (List; _∷_; [])
+open import Data.Nat          as ℕ       using (ℕ; suc; zero)
+open import Data.Product      as Product using (_×_; _,_)
 
 open import Reflection.AST
 open import Reflection.AST.Term
diff --git a/src/Tactic/RingSolver/Core/NatSet.agda b/src/Tactic/RingSolver/Core/NatSet.agda
@@ -36,10 +36,10 @@
 
 module Tactic.RingSolver.Core.NatSet where
 
-open import Data.Nat   as ℕ     using (ℕ; suc; zero)
-open import Data.List  as List  using (List; _∷_; [])
+open import Data.Nat        as ℕ     using (ℕ; suc; zero)
+open import Data.List.Base  as List  using (List; _∷_; [])
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
-open import Data.Bool  as Bool  using (Bool)
+open import Data.Bool       as Bool  using (Bool)
 open import Function
 open import Relation.Binary.PropositionalEquality
 
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
@@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition
 open import Data.Nat            as ℕ  using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Nat.Properties as ℕₚ using (≤′-trans)
 open import Data.Product              using (_,_; _×_; proj₂)
-open import Data.List                 using (_∷_; [])
+open import Data.List.Base            using (_∷_; [])
 open import Data.List.Kleene
 open import Data.Vec                  using (Vec)
 open import Function
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Base as ℕ                         using (ℕ; suc; zero;
 open import Data.Nat.Properties as ℕₚ                  using (≤′-trans)
 open import Data.Vec.Base as Vec                       using (Vec; _∷_)
 open import Data.Fin                                   using (Fin; zero; suc)
-open import Data.List                                  using (_∷_; [])
+open import Data.List.Base                             using (_∷_; [])
 open import Data.Unit using (tt)
 open import Data.List.Kleene
 open import Data.Product                               using (_,_; proj₁; proj₂; map₁; _×_)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
@@ -13,11 +13,11 @@ module Tactic.RingSolver.Core.Polynomial.Semantics
   (homo : Homomorphism r₁ r₂ r₃ r₄)
   where
 
-open import Data.Nat     using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
-open import Data.Vec     using (Vec; []; _∷_; uncons)
-open import Data.List    using ([]; _∷_)
-open import Data.Product using (_,_; _×_)
-open import Data.List.Kleene using (_+; _*; ∹_; _&_; [])
+open import Data.Nat          using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
+open import Data.Vec          using (Vec; []; _∷_; uncons)
+open import Data.List.Base    using ([]; _∷_)
+open import Data.Product      using (_,_; _×_)
+open import Data.List.Kleene  using (_+; _*; ∹_; _&_; [])
 
 open Homomorphism homo hiding (_^_)
 open import Tactic.RingSolver.Core.Polynomial.Base from
diff --git a/tests/data/appending/Main.agda b/tests/data/appending/Main.agda
@@ -3,7 +3,7 @@
 module Main where
 
 
-open import Data.List using (replicate)
+open import Data.List.Base using (replicate)
 open import Data.String using (toList; fromList)
 
 open import IO
diff --git a/tests/data/appending/TakeWhile.agda b/tests/data/appending/TakeWhile.agda
@@ -3,7 +3,7 @@
 module TakeWhile where
 
 open import Level
-open import Data.List hiding (takeWhile)
+open import Data.List.Base hiding (takeWhile)
 open import Data.List.Relation.Unary.All as List using ([]; _∷_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_; refl)
 open import Data.List.Relation.Ternary.Appending.Propositional
diff --git a/tests/data/list/Main.agda b/tests/data/list/Main.agda
@@ -3,7 +3,7 @@
 module Main where
 
 open import Level
-open import Data.List as List using (List; _∷_; []; _++_; reverse)
+open import Data.List.Base as List using (List; _∷_; []; _++_; reverse)
 open import Data.List.Zipper
 import Data.List.Sort as Sort
 open import Data.Maybe.Base
diff --git a/tests/data/trie/Main.agda b/tests/data/trie/Main.agda
@@ -7,14 +7,14 @@ module Main where
 open import Level
 open import Data.Unit
 open import Data.Bool
-open import Data.Char        as Char hiding (show)
-import Data.Char.Properties  as Char
-open import Data.List        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.String      as String using (String; unlines; _++_)
-open import Data.These       as These
+open import Data.Char         as Char hiding (show)
+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.String       as String using (String; unlines; _++_)
+open import Data.These        as These
 
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
