From 25d4df9182c92ef26979566f06c7c9f17746f0fb Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sun, 25 Nov 2018 11:29:53 +0100 Subject: port to agda/2.5.4.1 and agda-stdlib/0.17 --- FinMap.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'FinMap.agda') diff --git a/FinMap.agda b/FinMap.agda index 7380b71..df422c3 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -11,7 +11,7 @@ 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 -import Data.List.Any.Membership.Propositional +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) @@ -24,7 +24,7 @@ open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Generic using (just-injective) _∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set -_∈_ {A} x xs = x Data.List.Any.Membership.Propositional.∈ (toList xs) +_∈_ {A} x xs = Data.List.Membership.Setoid._∈_ (P.setoid A) x (toList xs) _∉_ : {A : Set} {n : ℕ} → A → Vec A n → Set _∉_ {A} x xs = All (_≢_ x) (toList xs) -- cgit v1.2.3