move imports for agda-stdlib 1.3
[~helmut/bidiragda.git] / FinMap.agda
index 1241252..76709c1 100644 (file)
@@ -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