Documentation

Finite number type. The type Finite n is inhabited by exactly n values in the range [0, n) including 0 but excluding n. Invariants:

getFinite x < natVal x

getFinite x >= 0

Convert an Integer into a Finite, throwing an error if the input is out of bounds.

Convert a Finite into the corresponding Integer.