[Agda] Fwd: Converting All2 to All

[Matthew Daggitt]

Gergo, thanks for your PR to the library with the proofs. I've updated the
library so they shouldn't cause the cyclic dependency any more.

On Sun, Jan 7, 2018 at 4:34 AM, Dr. ERDI Gergo <gergo at erdi.hu> wrote:

> On Sat, 6 Jan 2018, Matthew Daggitt wrote:
>
> 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.Extensional
>> Pointwise`.
>> Feel free to have a look at the CHANGELOG in standard library repository
>> for a more
>> detailed explanation.
>>
>
> Thanks, that is a very useful heads-up. I've now migrated my code to
> D.V.R.InductivePointwise in anticipation of this change.
>
> 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.
>>
>
> One snag, though, is that the current upgrade path of the stdlib requires
> D.V.All to import D.V.R.InductivePointwise, so I can't add these proofs to
> D.V.R.InductivePointwise without causing a circular import... the only
> place to add them currently is D.V.All. Would it still make sense for me to
> add them to D.V.All?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180110/175fb849/attachment.html>