move imports for agda-stdlib 1.3

1 files changed, 4 insertions, 4 deletions

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