[Agda] All P xs -> x in xs -> ..

Nils Anders Danielsson nad at cse.gu.se
Wed Oct 23 17:19:07 CEST 2013


On 2013-10-23 17:13, Sergei Meshveliani wrote:
> has Standard library something close to
>
>    all-P→Px :  ... (P Respects _≈_) → All P xs → x ∈ xs → P x
> ?

I don't think so. If _≈_ is _≡_, then you can use Data.List.All.lookup.

-- 
/NAD



More information about the Agda mailing list