[Agda] Fwd: Converting All2 to All

[Matthew Daggitt]

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


On Sat, Jan 6, 2018 at 6:26 AM, Dr. ERDI Gergo <gergo at erdi.hu> wrote:

> On Sat, 6 Jan 2018, Dr. ERDI Gergo wrote:
>
> 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
>>
>
> Of course there's a symmetric all₂₂ with (λ x y → P y)as well.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180106/06789a02/attachment.html>