[Agda] Strict application

[Andrés Sicard-Ramírez]

Hi Dmytro,

On 26 April 2014 08:42, Dmytro Starosud <d.starosud at gmail.com> wrote:

> That looks not really related to Agda itself, but to execution Agda code.
> I suppose you are using MAlonzo backend
>

I'm not thinking in execution of Agda code.

In the following code, foo normalises to 0 because the application is
non-strict. Using a strict application foo shouldn't normalise.

{-# NO_TERMINATION_CHECK #-}
loop : ℕ
loop = loop

foo : ℕ
foo = (λ _ → 0) loop

Best,

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140426/030cf025/attachment.html