Simplified Vec import (#2018)

Author: Sofia-Insa

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′)

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

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)

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

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)

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⇔)

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)

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)

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
 

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 ≡

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

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
 

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 (_+; _*; ∹_; _&_; [])

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