[Agda] More aggressive `with`: Please check your Agda-2.4.2
developments!
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Nov 19 14:16:52 CET 2015
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/
More information about the Agda
mailing list