Skip to content

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