Hi Gergo,

So the first thing to say is that due to an oversight, the functionality

of `Allâ` in `Data.Vec.All` is actually a duplicate of the existing

datatype `Relation.Binary.Vec.Pointwise`. In the upcoming release of the

library at the end of January, we're deprecating `Allâ` and moving

`Relation.Binary.Vec.Pointwise` to `Data.Vec.Relation.InductivePointwise`

and `Data.Vec.Relation.ExtensionalPointwise`. Feel free to have a look at

the CHANGELOG in standard library

<https://github.com/agda/agda-stdlib/tree/master/src> repository for a more

detailed explanation.

That's not to say your proofs wouldn't be a welcome contribution to the

library! The natural place for it in v0.15 will be in the new module

`Data.Vec.Relation.InductivePointwise`. I would probably name them

something like `pointwiseË¡âall` and `pointwiseÊ³âall`, and possibly add

their counterparts `allâpointwiseË¡` and `allâpointwiseÊ³` as well. If you'd

like to add them, feel free to submit a pull request to the library and

they can be added to the upcoming release.

Thanks,

Matthew

*Post by Dr. ERDI Gergo*allââ : â {a b} {A : Set a} {B : Set b} {P : A â Set}

*Post by Dr. ERDI Gergo*{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

Of course there's a symmetric allââ with (Î» x y â P y)as well.

_______________________________________________

Agda mailing list

https://lists.chalmers.se/mailman/listinfo/agda