<div dir="ltr"><div class="gmail_extra">Hi Dmytro,<br><br></div><div class="gmail_extra"><div class="gmail_quote">On 26 April 2014 08:42, Dmytro Starosud <span dir="ltr"><<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</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=":13y" class="" style="overflow:hidden">That looks not really related to Agda itself, but to execution Agda code.<br>
I suppose you are using MAlonzo backend</div></blockquote></div><br></div><div class="gmail_extra">I'm not thinking in execution of Agda code.<br><br></div><div class="gmail_extra">In the following code, foo normalises to 0 because the application is non-strict. Using a strict application foo shouldn't normalise.<br>
</div><div class="gmail_extra"><br>{-# NO_TERMINATION_CHECK #-}<br>loop : ℕ<br>loop = loop<br><br>foo : ℕ<br>foo = (λ _ → 0) loop<br></div><div class="gmail_extra"><br></div><div class="gmail_extra">Best,<br><br clear="all">
</div><div class="gmail_extra">-- <br><div dir="ltr">Andrés<br></div>
</div></div>