All P $ map f xs ←→ All (P ∘ f) xs

[mechvel]

Does Standard library need to implement

        all∘ :  ... →  All P (map f xs)  ←→ All (P ∘ f) xs

?
(is it somehow by All.map ?)

[andreasabel]

Isn't that already in Data.List.All.Properties ?

map-All : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
{f : A → B} {xs} →
All P (List.map f xs) → All (P ∘ f) xs
map-All {xs = []} [] = []
map-All {xs = _ ∷ _} (p ∷ ps) = p ∷ map-All ps

[mechvel]

On Sun, 2014-03-02 at 07:41 -0800, Andreas Abel wrote:

Isn't that already in Data.List.All.Properties ?

map-All : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
{f : A → B} {xs} →
All P (List.map f xs) → All (P ∘ f) xs
map-All {xs = []} [] = []
map-All {xs = _ ∷ _} (p ∷ ps) = p ∷ map-All ps

—
Reply to this email directly or view it on GitHub.

Yes, map-All and All-map do this.

Thank you.

---

Sergei