summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHelmut Grohne <helmut@subdivi.de>2022-08-18 15:41:00 +0200
committerHelmut Grohne <helmut@subdivi.de>2022-08-18 15:41:00 +0200
commit9c77e3515bc76994514eb1531e366e0cfa00651d (patch)
tree3d192677f6b8c56c4a9942f0fbc28373ba4146ad
parent1286deef698a9fbf92b86d0078fd62c47f980ee9 (diff)
downloadbidiragda-master.tar.gz
fix deprecation warning about Any.any with agda-stdlib 1.7.1HEADmaster
-rw-r--r--FinMap.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/FinMap.agda b/FinMap.agda
index 76709c1..62cf75f 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -32,7 +32,7 @@ data Dec∈ {A : Set} {n : ℕ} (x : A) (xs : Vec A n) : Set where
no-∉ : x ∉ xs → Dec∈ x xs
is-∈ : {A : Set} {n : ℕ} → Decidable (_≡_ {A = A}) → (x : A) → (xs : Vec A n) → Dec∈ x xs
-is-∈ eq? x xs with Any.any (eq? x) (toList xs)
+is-∈ eq? x xs with Any.any? (eq? x) (toList xs)
... | yes x∈xs = yes-∈ x∈xs
... | no x∉xs = no-∉ (Π._⟨$⟩_ (Surjection.to AllP.¬Any↠All¬) x∉xs)