| 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.
|
| Use_nat_1 |
Provides operations involving natural numbers (nat_1 values).
|
| Use_nat_2 |
Provides operations involving natural numbers (nat_2 values).
|
| Use_nat_3 |
Provides operations involving natural numbers (nat_3 values).
|