fix deprecation warning about Any.any with agda-stdlib 1.7.1 master
authorHelmut Grohne <helmut@subdivi.de>
Thu, 18 Aug 2022 13:41:00 +0000 (15:41 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 18 Aug 2022 13:41:00 +0000 (15:41 +0200)
FinMap.agda

index 76709c1..62cf75f 100644 (file)
@@ -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)