[Agda] `search' format

[Sergei Meshveliani]

Can people tell, please, 

what may be a sensible general format for searching in a list?

I consider this one: 

  search : ∀ {p} {P : A → Set p} → (P? : Decidable P) → (xs : List A) →
                        
                                         Found P? xs  ⊎  All (¬_ ∘ P) xs

where Found is defined as

  record Found {p} {P : A → Set p} (P? : Decidable P) (xs : List A) :
                                                                 Set _
         where
         field  prefix   : List A
                found    : A
                suffix   : List A
                ¬prefix  : All (¬_ ∘ P) prefix
                P-found  : P found
                concatEq : prefix ++ (found ∷ suffix) ≡ xs

I think this expresses completely the axioms for searching in a list. 

Has Standard library something similar?

(I am sorry if the list answered to this long ago, I just do not
recall).  

Thanks,

------
Sergei