<div dir="ltr"><div>This is a consequence of the new termination checking of with functions [1].<br></div>The problem in this case is that the termination checker doesn't see the relationship<br>between as and bs. I don't think this is a big problem though, since it's only an<br>
issue if you with-abstract over variables (or constructor patterns), which it doesn't<br>make much sense to do.<br><div><br></div><div>/ Ulf<br></div><div><br>[1] Issue 59: <a href="https://code.google.com/p/agda/issues/detail?id=59">https://code.google.com/p/agda/issues/detail?id=59</a><br>
</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Mar 25, 2014 at 9:31 PM, Mateusz Kowalczyk <span dir="ltr"><<a href="mailto:fuuzetsu@fuuzetsu.co.uk" target="_blank">fuuzetsu@fuuzetsu.co.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I'm running Agda 2.3.3, built yesterday. While trying to help someone in<br>
#agda, one of their functions was highlighted in salmon to indicate<br>
non-termination. We have stripped down the example to [1]. As you can<br>
see at [2], my emacs highlights filterN as potentially non-terminating<br>
but 2 people in #agda with Agda 2.3.2.2 report that the code is all<br>
fine. See a session screenshot from one of them at [3].<br>
<br>
Is this a regression or an improvement? What changed? Did older Agda<br>
admit a function it shouldn't have been or is this just a bug in newer Agda?<br>
<br>
Thanks<br>
<br>
[1]: <a href="http://lpaste.net/101716" target="_blank">http://lpaste.net/101716</a><br>
[2]: <a href="http://fuuzetsu.co.uk/images/1395779363.png" target="_blank">http://fuuzetsu.co.uk/images/1395779363.png</a><br>
[3]: <a href="http://i.imgur.com/2Iy1Gkx.png" target="_blank">http://i.imgur.com/2Iy1Gkx.png</a><br>
<span class="HOEnZb"><font color="#888888">--<br>
Mateusz K.<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>