move imports for agda-stdlib 1.3

6 files changed, 17 insertions, 17 deletions

diff --git a/Bidir.agda b/Bidir.agda
index e31d844..580b770 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -15,9 +15,9 @@ open import Data.Maybe.Relation.Binary.Pointwise using (just ; nothing ; drop-ju
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
 open import Data.List using (List)
-open import Data.List.All using (All)
+open import Data.List.Relation.Unary.All using (All)
 open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; allFin) renaming (lookup to lookupVec)
-open import Data.Vec.Relation.Pointwise.Inductive using (Pointwise)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise)
 open import Data.Vec.Properties using (lookup∘tabulate ; lookup∘update ; map-cong ; map-∘ ; map-lookup-allFin)
 open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
 open import Function using (id ; _∘_ ; flip)
@@ -25,7 +25,7 @@ open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSeto
 open import Relation.Binary.Indexed.Heterogeneous.Construct.At using (_atₛ_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; inspect ; [_] ; module ≡-Reasoning)
 open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
-import Relation.Binary.EqReasoning as EqR
+import Relation.Binary.Reasoning.Setoid as EqR
 
 open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped)
 open import Instances using (MaybeFunctor ; ShapedISetoid)
@@ -66,21 +66,21 @@ _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe
 _in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) (toList is)
 
 lemma-assoc-domain : {m n : ℕ} → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → is in-domain-of h
-lemma-assoc-domain []         []         ph = Data.List.All.[]
+lemma-assoc-domain []         []         ph = Data.List.Relation.Unary.All.[]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph with assoc is' xs' | inspect (assoc is') xs'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph')
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_
   (x' , lookup∘update i' h' (just x'))
-  (Data.List.All.map
+  (Data.List.Relation.Unary.All.map
     (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡)
     (lemma-assoc-domain is' xs' ph'))
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | just h' | [ ph' ] | ._ | _ | wrong _ _ _
 
 lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → {h' : FinMapMaybe m Carrier} → checkInsert i x h ≡ just h' → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h → map (flip lookupM h') js ≡ map (flip lookupM h) js
 lemma-map-lookupM-assoc i x h ph [] pj = P.refl
-lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = P.cong₂ _∷_
+lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.Relation.Unary.All._∷_ (x' , pl) pj) = P.cong₂ _∷_
   (P.trans (lemma-lookupM-checkInsert j i h pl x ph) (P.sym pl))
   (lemma-map-lookupM-assoc i x h ph js pj)
 
diff --git a/CheckInsert.agda b/CheckInsert.agda
index dbba6e6..68f5fdb 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -13,7 +13,7 @@ open import Data.Vec.Properties using (lookup∘update′)
 open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary using (Setoid ; module DecSetoid)
-import Relation.Binary.EqReasoning as EqR
+import Relation.Binary.Reasoning.Setoid as EqR
 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; inspect ; [_] ; module ≡-Reasoning)
 
 open import FinMap
diff --git a/FinMap.agda b/FinMap.agda
index 1241252..76709c1 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -9,16 +9,16 @@ open import Data.Fin.Properties using (_≟_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
 open import Data.Vec.Properties using (lookup∘update ; lookup∘update′ ; lookup-replicate ; tabulate-cong ; lookup∘tabulate)
 open import Data.Product using (_×_ ; _,_)
-open import Data.List.All as All using (All)
-import Data.List.All.Properties as AllP
-import Data.List.Any as Any
+open import Data.List.Relation.Unary.All as All using (All)
+import Data.List.Relation.Unary.All.Properties as AllP
+import Data.List.Relation.Unary.Any as Any
 import Data.List.Membership.Setoid
 open import Function using (id ; _∘_ ; flip ; const)
 open import Function.Equality using (module Π)
 open import Function.Surjection using (module Surjection)
 open import Relation.Nullary using (yes ; no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary.Core using (Decidable)
+open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; _≗_ ; module ≡-Reasoning)
 
 _∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set
diff --git a/Generic.agda b/Generic.agda
index ed9d4a4..bac09d8 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -9,7 +9,7 @@ open import Data.Maybe.Relation.Binary.Pointwise using (just ; nothing) renaming
 open import Data.Nat using (ℕ ; zero ; suc)
 open import Data.Product using (_×_ ; _,_)
 open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_)
-import Data.Vec.Relation.Pointwise.Inductive as VecEq
+import Data.Vec.Relation.Binary.Pointwise.Inductive as VecEq
 open import Data.Vec.Properties using (map-cong)
 open import Function using (_∘_ ; id ; flip)
 open import Function.Equality using (_⟶_)
diff --git a/Instances.agda b/Instances.agda
index a09e30d..e59d8a1 100644
--- a/Instances.agda
+++ b/Instances.agda
@@ -7,7 +7,7 @@ import Data.Maybe.Categorical
 open import Data.Nat using (ℕ)
 open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
 open import Data.Vec using (Vec)
-open import Data.Vec.Relation.Pointwise.Inductive using (Pointwise-≡⇒≡)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-≡⇒≡)
 open import Function using (_∘_ ; id)
 open import Relation.Binary using (Setoid ; module Setoid)
 open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSetoid to ISetoid)
diff --git a/Precond.agda b/Precond.agda
index 623c99f..34c24fd 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -1,4 +1,4 @@
-open import Relation.Binary.Core using (Decidable)
+open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality using (_≡_)
 
 module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
@@ -16,8 +16,8 @@ open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList)
 open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘ ; lookup-replicate ; tabulate-cong ; lookup∘tabulate ; lookup∘update′)
-import Data.List.All
-open import Data.List.Any using (here ; there)
+import Data.List.Relation.Unary.All
+open import Data.List.Relation.Unary.Any using (here ; there)
 open import Data.List.Membership.Setoid using (_∉_)
 open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
@@ -49,7 +49,7 @@ lemma-union-delete-fromFunc {is = []} h {g = g} p = _ , (tabulate-cong (λ f →
         ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩
       just (maybe′ id (g f) (lookupM f h)) ∎))
   where open ≡-Reasoning
-lemma-union-delete-fromFunc {n = n} {is = i ∷ is} h {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin
+lemma-union-delete-fromFunc {n = n} {is = i ∷ is} h {g = g} (Data.List.Relation.Unary.All._∷_ (x , px) ps) = _ , (begin
   union h (delete i (delete-many is (fromFunc g)))
     ≡⟨ tabulate-cong inner ⟩
   union h (delete-many is (fromFunc g))