<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 26 April 2014 10:28, Wolfram Kahl <span dir="ltr">&lt;<a href="mailto:kahl@cas.mcmaster.ca" target="_blank">kahl@cas.mcmaster.ca</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 class="">&gt; {-# NO_TERMINATION_CHECK #-}<br>
&gt; loop : ℕ<br>
&gt; loop = loop<br>
&gt;<br>
&gt; foo : ℕ<br>
&gt; foo = (λ _ → 0) loop<br>
<br>
</div>This is not Agda code (or, if you want, is is ``illegal Agda code&#39;&#39;):<br>
You are only allowed to use {-# NO_TERMINATION_CHECK #-}<br>
where you have a separate termination proof.<br>
</blockquote></div><br>I agree. That is ``illegal Agda code&#39;&#39;.<br><br>Let _≡_ be the propositional equality. I can formalise a non-strict<br>application (beta) by<br><br>postulate<br>  D    : Set<br>  app  : D → D → D<br>

  lam  : (D → D) → D<br>  beta : ∀ f a → app (lam f) a ≡ f a<br><br>Using the same approach, can I formalise a strict application?<br><br></div><div class="gmail_extra">Best,<br clear="all"></div><div class="gmail_extra">

<br>-- <br><div dir="ltr">Andrés<br></div>
</div></div>