[TYPES] Errata

eduardo@sol.lifia.info.unlp.edu.ar eduardo at sol.lifia.info.unlp.edu.ar
Fri Oct 17 16:58:48 EDT 2008


Quoting eduardo at sol.info.unlp.edu.ar:

>>>
>> As you pointed out, this is false; but the proof doesn't use this.
>> It relies on the following general observation:
>>
>>  if M[x:=N] N1 ... Nk is SN   and   if N is SN
>>  then (\x.M) N N1 ... Nk is also SN
>>
>> (This is true.)
>
> You, of course, require x to occur free in M.
>

Oops! Didn't notice the "and if N is SN".

    Sorry.
    E.


----------------------------------------------------------------
Este mensaje ha sido enviado utilizando IMP desde LIFIA.



More information about the Types-list mailing list