<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 26 April 2014 10:28, Wolfram Kahl <span dir="ltr"><<a href="mailto:kahl@cas.mcmaster.ca" target="_blank">kahl@cas.mcmaster.ca</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 class="">> {-# NO_TERMINATION_CHECK #-}<br>
> loop : ℕ<br>
> loop = loop<br>
><br>
> foo : ℕ<br>
> foo = (λ _ → 0) loop<br>
<br>
</div>This is not Agda code (or, if you want, is is ``illegal Agda code''):<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''.<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>