All P $ map f xs ←→ All (P ∘ f) xs about agda-stdlib HOT 2 CLOSED

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

from agda-stdlib.

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

from agda-stdlib.