| Nat_1 |
Provides type nat_1 : natural numbers (non-negative integers)
along with basic operations involving them - Here the construction is inductive :
a natural number is either zero or the successor of a natural number.
|
| Nat_2 |
Provides type nat_2 : natural numbers (non-negative integers)
along with basic operations involving them - Here the construction is inductive :
a natural number is zero or one or the successor of the successor of a natural number.
|
| Nat_3 |
Provides type nat_3 : natural numbers (non-negative integers)
along with basic operations involving them - Here the construction is inductive :
a natural number is zero or two times a non-zero natural number or the successor of
two times a natural number.
|