From cf83ee4f1fcb98b9dcd95e4f14a35e0019014e52 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Fri, 23 Jun 2023 12:13:52 -0400 Subject: [PATCH] Simplify `Data.List` imports to `Data.List.Base` --- README/Data/List/Relation/Binary/Pointwise.agda | 2 +- README/Data/List/Relation/Binary/Subset.agda | 2 +- README/Data/Tree/AVL.agda | 2 +- README/Data/Trie/NonDependent.agda | 2 +- README/Tactic/RingSolver.agda | 2 +- README/Text/Regex.agda | 2 +- src/Data/Fin/Permutation/Transposition/List.agda | 2 +- src/Data/List/Countdown.agda | 2 +- .../Binary/Sublist/Heterogeneous/Solver.agda | 2 +- .../List/Relation/Unary/AllPairs/Properties.agda | 2 +- src/Data/List/Relation/Unary/Grouped.agda | 2 +- src/Data/Tree/Binary/Zipper.agda | 2 +- src/Data/Vec/Functional/Properties.agda | 2 +- src/Data/Vec/Reflection.agda | 2 +- src/Reflection/AST/Show.agda | 2 +- src/Reflection/AST/Traversal.agda | 12 ++++++------ src/Tactic/MonoidSolver.agda | 10 +++++----- src/Tactic/RingSolver/Core/NatSet.agda | 6 +++--- .../Core/Polynomial/Homomorphism/Addition.agda | 2 +- .../Core/Polynomial/Homomorphism/Lemmas.agda | 2 +- .../RingSolver/Core/Polynomial/Semantics.agda | 10 +++++----- tests/data/appending/Main.agda | 2 +- tests/data/appending/TakeWhile.agda | 2 +- tests/data/list/Main.agda | 2 +- tests/data/trie/Main.agda | 16 ++++++++-------- 25 files changed, 47 insertions(+), 47 deletions(-) diff --git a/README/Data/List/Relation/Binary/Pointwise.agda b/README/Data/List/Relation/Binary/Pointwise.agda index 4932413ad4..da804f12c9 100644 --- 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 index 44ba3fa053..f6ef7690a1 100644 --- 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 index 1d14058ff8..7994afed41 100644 --- 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 index 09825c30c3..2387a71242 100644 --- 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 index cc1db1ad21..fdbea87bbf 100644 --- 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 index 5b4ce805c0..17d3fe45f9 100644 --- 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 index 42505de541..e69071dbfb 100644 --- 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 using (_∘_) diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda index 1ae0efc9b8..fde7439ebf 100644 --- 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 index 9066338e8a..2fe2447efb 100644 --- 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 index 391fee8f8b..009ac3ce75 100644 --- 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 index eceb6a80d0..51f3f28a17 100644 --- 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 index 76b2d9fd8e..0e5f4b8d05 100644 --- 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 index 0d2d08da83..9c4486be47 100644 --- 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 index 8b0fa7799f..0ea6473ff2 100644 --- 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 index ffe97352f4..f0291cf447 100644 --- 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 index de28c8db2a..2a14fa628b 100644 --- a/src/Reflection/AST/Traversal.agda +++ b/src/Reflection/AST/Traversal.agda @@ -11,12 +11,12 @@ open import Effect.Applicative using (RawApplicative) 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.Product using (_×_; _,_) -open import Data.String using (String) -open import Function using (_∘_) -open import Reflection hiding (pure) +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Data.List.Base using (List; []; _∷_; _++_; reverse; length) +open import Data.Product using (_×_; _,_) +open import Data.String using (String) +open import Function using (_∘_) +open import Reflection hiding (pure) open RawApplicative AppF diff --git a/src/Tactic/MonoidSolver.agda b/src/Tactic/MonoidSolver.agda index e34d770cde..fcf193244b 100644 --- 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 index 485539792e..7ebbcebc22 100644 --- 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 index 990d6a46ed..d04ecbc131 100644 --- 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 index f0c5dfcd76..ce20b1e381 100644 --- 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 index 648563112d..8cde662620 100644 --- 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 index 93ece5eda0..0ba5618dc8 100644 --- 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 index 9030fb3c0c..5a885c3fbe 100644 --- 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 index f2b11de8ae..f7f12cd63d 100644 --- 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 index 4eab3cfd40..9dfac5cb26 100644 --- 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