Dr. ERDI Gergo

1970-01-01 00:00:00 UTC

I've written the following function for Data.Vect.All (but it would apply

just the same for Data.List.All):

allââ : â {a b} {A : Set a} {B : Set b} {P : A â Set}

{n} {xs : Vec A n} {ys : Vec B n} â

Allâ (Î» x y â P x) xs ys â All P xs

allââ [] = []

allââ (p â· ps) = p â· allââ ps

My questions are:

1. What would be a good name for this function? (I am fairly certain allââ

is not one:))

2. Should I add it to the stdlib?

Thanks,

Gergo

just the same for Data.List.All):

allââ : â {a b} {A : Set a} {B : Set b} {P : A â Set}

{n} {xs : Vec A n} {ys : Vec B n} â

Allâ (Î» x y â P x) xs ys â All P xs

allââ [] = []

allââ (p â· ps) = p â· allââ ps

My questions are:

1. What would be a good name for this function? (I am fairly certain allââ

is not one:))

2. Should I add it to the stdlib?

Thanks,

Gergo