From 3376eb8b4009e87500ebc311ab92c20a5999d207 Mon Sep 17 00:00:00 2001
From: Jakob Naucke <jakob.naucke@posteo.de>
Date: Sat, 20 Apr 2024 11:56:29 +0200
Subject: [PATCH] Add an Any type

to complement All
---
 lib/Haskell/Prelude.agda | 6 ++++--
 lib/Haskell/Prim.agda    | 5 +++++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
index a0bb63e8..70b6d560 100644
--- a/lib/Haskell/Prelude.agda
+++ b/lib/Haskell/Prelude.agda
@@ -5,8 +5,10 @@ open import Haskell.Prim
 open Haskell.Prim public using
   ( Bool; True; False; Char; Integer;
     List; []; _∷_; Nat; zero; suc; ⊤; tt;
-    TypeError; ⊥; iNumberNat; IsTrue; IsFalse;
-    All; allNil; allCons; NonEmpty; lengthNat;
+    TypeError; ⊥; iNumberNat; lengthNat;
+    IsTrue; IsFalse; NonEmpty;
+    All; allNil; allCons;
+    Any; anyHere; anyThere;
     id; _∘_; _$_; flip; const;
     if_then_else_; case_of_;
     Number; fromNat; Negative; fromNeg;
diff --git a/lib/Haskell/Prim.agda b/lib/Haskell/Prim.agda
index 65f6e3f5..94426a8c 100644
--- a/lib/Haskell/Prim.agda
+++ b/lib/Haskell/Prim.agda
@@ -110,6 +110,11 @@ data All {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
     allNil  : All B []
     allCons : ∀ {x xs} ⦃ i : B x ⦄ ⦃ is : All B xs ⦄ → All B (x ∷ xs)
 
+data Any {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
+  instance
+    anyHere  : ∀ {x xs} ⦃ i : B x ⦄ → Any B (x ∷ xs)
+    anyThere : ∀ {x xs} ⦃ is : Any B xs ⦄ → Any B (x ∷ xs)
+
 data IsTrue : Bool → Set where
   instance itsTrue : IsTrue True