[Agda] Strict application

[Wolfram Kahl]

On Sat, Apr 26, 2014 at 09:02:59AM -0500, Andrés Sicard-Ramírez wrote:
> 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

This is not Agda code (or, if you want, is is ``illegal Agda code''):
You are only allowed to use {-# NO_TERMINATION_CHECK #-}
where you have a separate termination proof.

;-)


Best,

Wolfram