[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