add search function to Data.List.Relation.Unary.All

CHANGELOG.md

@@ -32,6 +32,11 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Data.List.Relation.Unary.All`:
+  ```agda
+  search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
+  ```
+
 * In `Data.List.Relation.Binary.Equality.Setoid`:
   ```agda
   ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs

src/Data/List/Relation/Unary/All.agda

@@ -14,7 +14,7 @@ open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_)
 import Data.List.Membership.Setoid as SetoidMembership
 open import Data.Product.Base as Product
   using (∃; -,_; _×_; _,_; proj₁; proj₂; uncurry)
-open import Data.Sum.Base as Sum using (inj₁; inj₂)
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Effect.Applicative
 open import Effect.Monad
 open import Function.Base using (_∘_; _∘′_; id; const)
@@ -232,6 +232,9 @@ decide p∪q (x ∷ xs) with p∪q x
 ... | inj₂ qx = inj₂ (here qx)
 ... | inj₁ px = Sum.map (px ∷_) there (decide p∪q xs)
 
+search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
+search P? = decide (Sum.swap ∘ Dec.toSum ∘ P?)
+
 ------------------------------------------------------------------------
 -- DEPRECATED
 ------------------------------------------------------------------------