From ab79a2e7b7c10306493cb6e61eb10f3b4e114cf3 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 1 Jan 2018 19:51:00 +0100 Subject: fix compilation with agda 2.5.3, agda-stdlib 0.14 --- FinMap.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'FinMap.agda') diff --git a/FinMap.agda b/FinMap.agda index ca7e73b..3786b97 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -11,6 +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 open import Function using (id ; _∘_ ; flip ; const) open import Function.Equality using (module Π) open import Function.Surjection using (module Surjection) @@ -23,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 = Any.Membership._∈_ (P.setoid A) x (toList xs) +_∈_ {A} x xs = x Data.List.Any.Membership.Propositional.∈ (toList xs) _∉_ : {A : Set} {n : ℕ} → A → Vec A n → Set _∉_ {A} x xs = All (_≢_ x) (toList xs) -- cgit v1.2.3