Natural Numbers, or the best way to enumerate anything 'utils require import Try It Out > Required module: utils 'Nat_context [ { Type '.Nat } { .Nat '.zero } { .Nat 'n -> .Nat ? '.succ } ] def Try It Out > 'Nat Nat_context { .Nat } prods "Natural" defconstr 'zero Nat_context { .zero } funs "0" defconstr Nat 'n -> 'succ Nat_context { .succ ( n ( .Nat .zero .succ ) ) } funs "S n" defconstr ! Try It Out > The Nat type is defined to \(Natural\) Nat tex. \(λ(\mathrm{n}:Natural).\,\mu(\mathrm{n})\) Nat ’n recursor dup tex has type \(∀(\mathrm{n}:Natural)\,(\mathrm{Nat}^P:Natural \rightarrow Set_{1}),\,\mathrm{Nat}^P\,0 \rightarrow (∀(\mathrm{n}_{0}:Natural),\,\mathrm{Nat}^P\,\mathrm{n}_{0} \rightarrow \mathrm{Nat}^P\,(S\,\mathrm{n}_{0})) \rightarrow \mathrm{Nat}^P\,\mathrm{n}\) type tex. \(λ(\mathrm{n}:Natural).\,S\,\mathrm{n}\) succ dup tex has type \(Natural \rightarrow Natural\) type tex.