<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 4 July 2014 13:26, 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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div id=":q7" class="" style="overflow:hidden">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.</div></blockquote></div><br></div>I guess that using an abstract block + NO_TERMINATION_CHECK should be enough.<br><div><div class="gmail_extra"><br>-- <br><div dir="ltr">Andrés<br></div>


</div></div></div>