A | |
| add [Use_nat_3] |
Adds two natural numbers.
|
| add [Use_nat_2] |
Adds two natural numbers.
|
| add [Use_nat_1] |
Adds two natural numbers.
|
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.
|
G | |
| greater_than [Use_nat_1] |
Tests whether m > n given the pair (m, n) of natural numbers.
|
H | |
| half [Use_nat_2] |
Returns the half of a natural number.
|
I | |
| int_of_nat [Use_nat_1] |
Converts a nat_1 value to a non-negative int value.
|
| inv_d0 [Nat_3] |
The inverse of the function d0.
|
| inv_d1 [Nat_3] |
The inverse of the function d1.
|
| is_even [Use_nat_2] |
Tests whether a natural number is even.
|
| 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_power_of_two [Use_nat_3] |
Tests whether a natural number is a power of two.
|
| is_zero [Use_nat_3] |
Tests whether a natural number is zero.
|
| is_zero [Nat_2] |
Tests whether a naturel number is zero.
|
| is_zero [Nat_1] |
Tests whether a naturel number is zero.
|
M | |
| mult [Use_nat_1] |
Multiplies two natural numbers.
|
N | |
| nat_of_int [Use_nat_3] |
Converts a non-negative int value to a nat_3 value.
|
| nat_of_int [Use_nat_2] |
Converts a non-negative int value to a nat_2 value.
|
| nat_of_int [Use_nat_1] |
Converts a non-negative int value to a nat_1 value.
|
O | |
| one [Nat_2] |
Constructs the natural number one.
|
P | |
| pre [Use_nat_3] |
Returns the predecessor of non-zero natural number.
|
| pre [Use_nat_2] |
Returns the predecessor of non-zero natural number.
|
| 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 | |
| subtract [Use_nat_1] |
Returns the natural number m - n given the pair (m, n) of natural numbers.
|
| suc [Use_nat_3] |
Returns the successor of a natural number.
|
| suc [Use_nat_2] |
Returns the successor of a natural number.
|
| suc [Nat_1] |
Constructs the successor of a natural number.
|
| sucsuc [Nat_2] |
Constructs the successor of the successor of a natural number.
|
T | |
| two_times [Use_nat_2] |
Returns two times 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.
|