Add an Any type

to complement All
naucke · Apr 20, 2024 · 3376eb8 · 3376eb8
1 parent 7b3e48a
commit 3376eb8
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git 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
@@ -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