[Agda] Non-termination change in Agda 2.3.3

[Ulf Norell]

This is a consequence of the new termination checking of with functions [1].
The problem in this case is that the termination checker doesn't see the
relationship
between as and bs. I don't think this is a big problem though, since it's
only an
issue if you with-abstract over variables (or constructor patterns), which
it doesn't
make much sense to do.

/ Ulf

[1] Issue 59: https://code.google.com/p/agda/issues/detail?id=59


On Tue, Mar 25, 2014 at 9:31 PM, Mateusz Kowalczyk
<fuuzetsu at fuuzetsu.co.uk>wrote:

> Hi,
>
> I'm running Agda 2.3.3, built yesterday. While trying to help someone in
> #agda, one of their functions was highlighted in salmon to indicate
> non-termination. We have stripped down the example to [1]. As you can
> see at [2], my emacs highlights filterN as potentially non-terminating
> but 2 people in #agda with Agda 2.3.2.2 report that the code is all
> fine. See a session screenshot from one of them at [3].
>
> Is this a regression or an improvement? What changed? Did older Agda
> admit a function it shouldn't have been or is this just a bug in newer
> Agda?
>
> Thanks
>
> [1]: http://lpaste.net/101716
> [2]: http://fuuzetsu.co.uk/images/1395779363.png
> [3]: http://i.imgur.com/2Iy1Gkx.png
> --
> Mateusz K.
> _______________________________________________
> 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/20140326/69cb3dcc/attachment.html