<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">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</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&#39;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>