Simplified Vec import (#2018)

agda · Jul 31, 2023 · bfa4f8b · bfa4f8b
1 parent f076d59
commit bfa4f8b
Show file tree

Hide file tree

Showing 14 changed files with 15 additions and 14 deletions.
diff --git a/README/Data/Tree/AVL.agda b/README/Data/Tree/AVL.agda
@@ -22,7 +22,7 @@ import Data.Tree.AVL
 open import Data.Nat.Properties using (<-strictTotalOrder)
 open import Data.Product as Prod using (_,_; _,′_)
 open import Data.String.Base using (String)
-open import Data.Vec using (Vec; _∷_; [])
+open import Data.Vec.Base using (Vec; _∷_; [])
 open import Relation.Binary.PropositionalEquality
 
 open Data.Tree.AVL <-strictTotalOrder renaming (Tree to Tree′)

diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Binary.Properties
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Data.Vec using ([]; _∷_)
+open import Data.Vec.Base using ([]; _∷_)
 open import Function.Base using (_∘_; _$_)
 open import Level using (0ℓ)
 open import Relation.Binary

diff --git a/src/Data/Vec/Bounded.agda b/src/Data/Vec/Bounded.agda
@@ -10,7 +10,8 @@ module Data.Vec.Bounded where
 
 open import Level using (Level)
 open import Data.Nat.Base
-open import Data.Vec as Vec using (Vec)
+open import Data.Vec.Base using (Vec)
+import Data.Vec as Vec using (filter; takeWhile; dropWhile)
 open import Function.Base using (id)
 open import Relation.Binary using (_Preserves_⟶_)
 open import Relation.Unary using (Pred; Decidable)

diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
@@ -16,7 +16,7 @@ open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
 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)
+open import Data.Vec.Base as V using (Vec)
 import Data.Vec.Properties as Vₚ
 open import Data.Vec.Functional
 open import Function.Base

diff --git a/src/Data/Vec/Membership/Propositional/Properties.agda b/src/Data/Vec/Membership/Propositional/Properties.agda
@@ -10,7 +10,7 @@ module Data.Vec.Membership.Propositional.Properties where
 
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Product as Prod using (_,_; ∃; _×_; -,_)
-open import Data.Vec hiding (here; there)
+open import Data.Vec.Base
 open import Data.Vec.Relation.Unary.Any using (here; there)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)

diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda
@@ -12,8 +12,8 @@ open import Data.Empty
 open import Data.Nat using (ℕ; suc)
 import Data.Nat.Properties as ℕ
 open import Data.Product using (_×_; _,_; proj₁; proj₂; uncurry)
+open import Data.Vec.Base using (Vec; []; _∷_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
-open import Data.Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
 open import Function.Base using (flip)
 open import Function.Bundles using (_⇔_; mk⇔)

diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
@@ -15,7 +15,7 @@ open import Data.Empty
 open import Data.Unit using (⊤; tt)
 open import Data.Product using (proj₁; proj₂)
 open import Data.Nat using (ℕ)
-open import Data.Vec using (Vec; []; _∷_)
+open import Data.Vec.Base using (Vec; []; _∷_)
 import Data.Vec.Relation.Binary.Lex.Strict as Strict
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
  using (Pointwise; []; _∷_; head; tail)

diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda
@@ -16,7 +16,7 @@ import Data.List.Relation.Unary.Any as List
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
 open import Data.Product as Prod using (∃; ∃₂; _×_; _,_; proj₁; proj₂)
-open import Data.Vec hiding (here; there)
+open import Data.Vec.Base hiding (here; there)
 open import Data.Vec.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Vec.Membership.Propositional
  using (_∈_; mapWith∈; find; lose)

diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Properties as ℕₚ using (≤′-trans)
 open import Data.Product.Base using (_,_; _×_; proj₂)
 open import Data.List.Base using (_∷_; [])
 open import Data.List.Kleene
-open import Data.Vec  using (Vec)
+open import Data.Vec.Base using (Vec)
 open import Function.Base using (_⟨_⟩_; flip)
 open import Relation.Unary
 

diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
@@ -18,7 +18,7 @@ open import Function.Base using (_⟨_⟩_)
 open import Data.Nat.Base as ℕ using (ℕ; suc; zero; compare)
 open import Data.Product.Base using (_,_; _×_; proj₁; proj₂)
 open import Data.List.Kleene
-open import Data.Vec using (Vec)
+open import Data.Vec.Base using (Vec)
 
 import Data.Nat.Properties as ℕ-Prop
 import Relation.Binary.PropositionalEquality.Core as ≡

diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Properties using (≤′-trans)
 open import Data.Nat.Induction
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; map₁)
 open import Data.List.Kleene
-open import Data.Vec  using (Vec)
+open import Data.Vec.Base using (Vec)
 open import Function.Base using (_⟨_⟩_; flip)
 open import Induction.WellFounded
 open import Relation.Unary

diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
@@ -13,8 +13,8 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where
 
+open import Data.Vec.Base using (Vec)
 open import Data.Product.Base using (_,_)
-open import Data.Vec using (Vec)
 open import Data.Nat using (_<′_)
 open import Data.Nat.Induction
 

diff --git a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
@@ -14,7 +14,7 @@ module Tactic.RingSolver.Core.Polynomial.Semantics
  where
 
 open import Data.Nat using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
-open import Data.Vec  using (Vec; []; _∷_; uncons)
+open import Data.Vec.Base using (Vec; []; _∷_; uncons)
 open import Data.List.Base using ([]; _∷_)
 open import Data.Product.Base using (_,_; _×_)
 open import Data.List.Kleene using (_+; _*; ∹_; _&_; [])

diff --git a/src/Tactic/RingSolver/NonReflective.agda b/src/Tactic/RingSolver/NonReflective.agda
@@ -24,7 +24,7 @@ open import Data.Maybe.Base
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product
-open import Data.Vec hiding (_⊛_)
+open import Data.Vec.Base using (Vec)
 open import Data.Vec.N-ary
 
 open import Tactic.RingSolver.Core.Polynomial.Parameters