- N = ∀ α . (α->α)->α->α;
- Pair = (N -> N -> N) -> N;
- let zero = lambda α . lambda s:α->α . lambda z:α. z in
- let fst = lambda x:N . lambda y:N . x in
- let snd = lambda x:N . lambda y:N . y in
- let pair = lambda x:N . lambda y:N . lambda z:N->N->N . z x y in
- let suc = lambda n:N . lambda α . lambda s:α->α . lambda z:α . s (n [α] s z) in
- let shift = lambda p:Pair . pair (suc (p fst)) (p fst) in
- let pre = lambda n:N . n [Pair] shift (pair zero zero) snd in
+ N = ∀α. (α->α)->α->α;
+ Pair = (N->N->N) -> N;
+ let zero = α . λs:α->α . λz:α. z in
+ let fst = λx:N . λy:N . x in
+ let snd = λx:N . λy:N . y in
+ let pair = λx:N . λy:N . λz:N->N->N . z x y in
+ let suc = λn:N . λα . λlambda s:α->α . λz:α . s (n [α] s z) in
+ let shift = λp:Pair . pair (suc (p fst)) (p fst) in
+ let pre = λn:N . n [Pair] shift (pair zero zero) snd in