[Agda] Fwd: Converting All2 to All

Matthew Daggitt matthewdaggitt at gmail.com
Wed Jan 10 23:00:39 CET 2018


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>


More information about the Agda mailing list