D | |
| d0 [Nat_3] |
Constructs the natural number that is two times a non-zero natural number.
|
| d1 [Nat_3] |
Constructs the natural number that is the successor of two times a natural number.
|
I | |
| inv_d0 [Nat_3] |
The inverse of the function d0.
|
| inv_d1 [Nat_3] |
The inverse of the function d1.
|
| is_even_non_zero [Nat_3] |
Test whether a natural number is even and non-zero.
|
| is_odd [Nat_3] |
Test whether a natural number is odd.
|
| is_one [Nat_2] |
Tests whether a naturel number is one.
|
| is_zero [Nat_2] |
Tests whether a naturel number is zero.
|
| is_zero [Nat_1] |
Tests whether a naturel number is zero.
|
O | |
| one [Nat_2] |
Constructs the natural number one.
|
P | |
| pr_nat [Nat_3] | |
| pr_nat [Nat_2] | |
| pr_nat [Nat_1] | |
| pre [Nat_1] |
Returns the predecessor of non-zero natural number.
|
| prepre [Nat_2] |
Returns the predecessor of the predecessor of natural number greater than one.
|
| print_nat [Nat_3] |
Prints a string representation of a natural number.
|
| print_nat [Nat_2] |
Prints a string representation of a natural number.
|
| print_nat [Nat_1] |
Prints a string representation of a natural number.
|
S | |
| suc [Nat_1] |
Constructs the successor of a natural number.
|
| sucsuc [Nat_2] |
Constructs the successor of the successor of a natural number.
|
Z | |
| zero [Nat_3] |
Constructs the natural number zero.
|
| zero [Nat_2] |
Constructs the natural number zero.
|
| zero [Nat_1] |
Constructs the natural number zero.
|