summaryrefslogtreecommitdiff
path: root/FinMap.agda
diff options
context:
space:
mode:
authorHelmut Grohne <helmut@subdivi.de>2018-01-01 19:51:00 +0100
committerHelmut Grohne <helmut@subdivi.de>2018-01-01 19:51:00 +0100
commitab79a2e7b7c10306493cb6e61eb10f3b4e114cf3 (patch)
tree923efedbb0b74075d8efb66ba4b5b33dd4ed3cc2 /FinMap.agda
parentad721d4770c02769a9b7afab90160d1818afe1d6 (diff)
downloadbidiragda-ab79a2e7b7c10306493cb6e61eb10f3b4e114cf3.tar.gz
fix compilation with agda 2.5.3, agda-stdlib 0.14
Diffstat (limited to 'FinMap.agda')
-rw-r--r--FinMap.agda3
1 files changed, 2 insertions, 1 deletions
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)