port to agda/2.5.4.1 and agda-stdlib/0.17
[~helmut/bidiragda.git] / FinMap.agda
index 7380b71..df422c3 100644 (file)
@@ -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)