<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jul 4, 2014 at 8:26 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Objection, Ulf.<br>
<br>
NO_TERMINATION_CHECK is --no-termination-check, but for single definitions only. The semantics should stay as is.<br>
<br>
If you want to declare a definition as non-terminating, please add a new pragma, like<br>
<br>
{-# NON_TERMINATING bla #-}<br>
<br>
which informs Agda to not unfold bla.<br></blockquote><div><br></div><div>Ok, fine. I guess we can have both. I do think that my version is more important to have though. Disabling the termination checker and treating definitions as terminating anyway is a hack that shouldn't be encouraged. My version can be used safely (and soundly if paired with and inhabitation check).</div>
<div><br></div><div>/ Ulf</div></div></div></div>