Nat
Functions for converting between nat values and the ordinary integer
representation of the natural numbers.
The built-in nat type is defined as:
type nat
= Zero
| Succ(nat)
Note that it is not necessary to use pack explicitly when working with
numeric literals. For example, you can write:
let
x : nat = 5
in
and the compiler will perform the conversion automatically. This works because numeric literals are overloaded.
pack
Convert an int64 value into a natural number.
Interpret the given integer as a natural number and return the
corresponding nat value. If the input is negative, the function
will return Zero.
pack : int64 -> natpack : int64 -> nat
unpack
Convert a natural number into an int64 value.
Return the integer representation of the given value as an int64.
unpack : nat -> int64unpack : nat -> int64
Natural
trait
Trait that comprises types that can be converted to nat, via:
to_nat : n -> nat