<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 4 July 2014 13:26, 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: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>