[Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!

[Ulf Norell]

agda-prelude: no breakage

/ Ulf

On Thu, Nov 19, 2015 at 2:16 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> Dear Agda users and developers,
>
> please check your larger Agda-2.4.2 developments with the version at
>
>   https://github.com/andreasabel/agda-issue-1692/tree/maint-2.4.2
>
> You can get it with
>
>   git clone https://github.com/andreasabel/agda-issue-1692.git
>   cd agda-issue-1692
>   git checkout maint-2.4.2
>   make install-bin
>
> This version is making `with` more agressive and hopefully more intuitive
> (at least it removes the stumbling block reported in issue #1692).
>
> The change is not fully backwards compatible. However, the breakage should
> be small. Nothing broke for the std-lib. Only a single test case broke,
> which uses with on a function argument (a variable):
>
> https://github.com/agda/agda/blob/master/test/lib-succeed/Issue846/DivModUtils.agda#L99
> The breakage was easy to fix, the new `with` is simpler: the `with` on the
> variable could be removed.
>
> Please check the amount of breakage on your Agda developments and report
> back, with self-contained test-cases (e.g. as tar-balls and repo links) on
>
>   https://github.com/agda/agda/issues/1692
>
> This let's me evaluate whether this commit can go into the maintenance
> version or not (in case the breakage is too big).
>
> Response time: 5 work days.
>
> Cheers,
> Andreas
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> 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/20151120/2e4c3783/attachment-0001.html