diff options
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 8 |
1 files changed, 4 insertions, 4 deletions
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 |