[CST-2] Types

[Alvin]

Hello!

Just a wee question on PLC datatypes.  1998 Paper 7 Question 10 - the second
part basically asks for a PLC representation of the successor function -
s(n) = n+1.  This is probably very easy, but I'm just not sure how to encode
the addition of 1 in PLC, is this actually significant as it doesn't alter
the type?  Very confused.

Anyway, I've got as far as typing the natural numbers

nat = !a(a->(a->a)->a)

And the beginning of succ

Succ = /\a(Lx:nat( what goes in here? X+1?))

Cheers

Alvin