Kind/book/Nat/succ.kind2
2024-07-08 18:13:17 -03:00

6 lines
49 B
Plaintext

succ
- n: Nat
: Nat
~λP λsucc λzero (succ n)