finite-typelits-0.2.1.0: A type inhabited by finitely many values, indexed by type-level naturals

Copyright	(C) 2022-2023 mniip
License	BSD3
Maintainer	mniip <[email protected]>
Stability	experimental
Portability	portable
Safe Haskell	None
Language	Haskell2010

Data.Finite.Internal

Description

Synopsis

type Finite = Finite Integer
pattern Finite :: Integer -> Finite n
finite :: forall (n :: Nat). KnownNat n => Integer -> Finite n
getFinite :: forall (n :: Nat). Finite n -> Integer

Documentation

type Finite = Finite Integer Source #

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 :: Integer -> Finite n Source #

finite :: forall (n :: Nat). KnownNat n => Integer -> Finite n Source #

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

getFinite :: forall (n :: Nat). Finite n -> Integer Source #

Convert a Finite into the corresponding Integer.