> And the beginning of succ
>
> Succ = /\a(Lx:nat( what goes in here? X+1?))
Succ = /\a(Ln:nat(Lx:a(Lf:a->a(f(n a x f)))))
Mat
Matej Pfajfar
St John's College, University of Cambridge, UK
GPG Public Key @ http://matejpfajfar.co.uk/keys
Most people are good people, the rest of us are going to
run the world. -- badbytes
WARNING: THIS E-MAIL ACCOUNT WILL BE DELETED ON
30/09/2002. PLEASE USE mp@cantab.net.