Data.Finite.Internal

Documentation

type Finite = Finite Integer

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

pattern Finite :: forall n. Integer -> Finite n

finite :: forall n. KnownNat n => Integer -> Finite n

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

getFinite :: forall n. Finite n -> Integer

Convert a Finite into the corresponding Integer.