[Agda] Normalisation before termination checking

[Nils Anders Danielsson]

On Wed, Jul 23, 2008 at 10:23 AM, Arnaud Spiwack
<Arnaud.Spiwack at lix.polytechnique.fr> wrote:
>
> Note that you must be careful when doing that, if you are interested in
> Strong Normalisation :
> F x = ( \ y . 0 ) ( F x )
>
> Is weakly normalisable but not strongly normalisable, whereas    F x = 0
>  (which is what you are testing after normalising the right-hand side) is
> both.

If we take the actual program to be the one after normalisation, then
we still get strong normalisation, unless I have missed something else
as well. This could be undesirable for other reasons, though.

-- 
/NAD