From 9c77e3515bc76994514eb1531e366e0cfa00651d Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 18 Aug 2022 15:41:00 +0200 Subject: fix deprecation warning about Any.any with agda-stdlib 1.7.1 --- FinMap.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -- cgit v1.2.3