<div dir="ltr">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.</div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jan 7, 2018 at 4:34 AM, Dr. ERDI Gergo <span dir="ltr"><<a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Sat, 6 Jan 2018, Matthew Daggitt wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Gergo, So the first thing to say is that due to an oversight, the functionality of<br>
`All₂` in `Data.Vec.All` is actually a duplicate of the existing datatype<br>
`Relation.Binary.Vec.Pointwise<wbr>`. In the upcoming release of the library at the end of<br>
January, we're deprecating `All₂` and moving `Relation.Binary.Vec.Pointwise<wbr>` to<br>
`Data.Vec.Relation.InductivePo<wbr>intwise` and `Data.Vec.Relation.Extensional<wbr>Pointwise`.<br>
Feel free to have a look at the CHANGELOG in standard library repository for a more<br>
detailed explanation.<br>
</blockquote>
<br></span>
Thanks, that is a very useful heads-up. I've now migrated my code to D.V.R.InductivePointwise in anticipation of this change.<span class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
That's not to say your proofs wouldn't be a welcome contribution to the library! The<br>
natural place for it in v0.15 will be in the new module<br>
`Data.Vec.Relation.InductivePo<wbr>intwise`. I would probably name them something<br>
like `pointwiseˡ⇒all` and `pointwiseʳ⇒all`, and possibly add their counterparts<br>
`all⇒pointwiseˡ` and `all⇒pointwiseʳ` as well. If you'd like to add them, feel free<br>
to submit a pull request to the library and they can be added to the upcoming release.<br>
</blockquote>
<br></span>
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?</blockquote></div><br></div>