Modulefinite-typelits-0.2.0.0Haskell2010

Data.Finite.Internal

typetype 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:

Property

prop> getFinite x < natVal x

Property

prop> getFinite x >= 0

patternpattern Finite :: Integer -> Finite n

valuefinite :: KnownNat n => Integer -> Finite n

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

valuegetFinite :: Finite n -> Integer

Convert a Finite into the corresponding Integer.