module Use_nat_2: sig .. end
Provides operations involving natural numbers (nat_2 values).
val is_even : Nat_2.nat_2 -> bool
Tests whether a natural number is even.
val two_times : Nat_2.nat_2 -> Nat_2.nat_2
Returns two times a natural number.
val suc : Nat_2.nat_2 -> Nat_2.nat_2
Returns the successor of a natural number.
val half : Nat_2.nat_2 -> Nat_2.nat_2
Returns the half of a natural number.
val add : Nat_2.nat_2 * Nat_2.nat_2 -> Nat_2.nat_2
Adds two natural numbers.
val pre : Nat_2.nat_2 -> Nat_2.nat_2
Returns the predecessor of non-zero natural number.
- Error if the number is zero.
val nat_of_int : int -> Nat_2.nat_2
Converts a non-negative int value to a nat_2 value.