From 1286deef698a9fbf92b86d0078fd62c47f980ee9 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sat, 1 Aug 2020 09:12:17 +0200 Subject: move imports for agda-stdlib 1.3 --- FinMap.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'FinMap.agda') 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 -- cgit v1.2.3