Copyright	(C) 2015-2022 mniip
License	BSD3
Maintainer	mniip <mniip@mniip.com>
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Finite.Internal

Description

Synopsis

newtype Finite (n :: Nat) = Finite Integer
finite :: KnownNat n => Integer -> Finite n
getFinite :: Finite n -> Integer

Documentation

newtype Finite (n :: Nat) Source #

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

getFinite x < natVal x

getFinite x >= 0

Constructors

Finite Integer

Instances

Instances details

KnownNat n => Bounded (Finite n) Source #	Throws an error for `Finite 0`
Instance details Defined in Data.Finite.Internal Methods minBound :: Finite n Source # maxBound :: Finite n Source #
KnownNat n => Enum (Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods succ :: Finite n -> Finite n Source # pred :: Finite n -> Finite n Source # toEnum :: Int -> Finite n Source # fromEnum :: Finite n -> Int Source # enumFrom :: Finite n -> [Finite n] Source # enumFromThen :: Finite n -> Finite n -> [Finite n] Source # enumFromTo :: Finite n -> Finite n -> [Finite n] Source # enumFromThenTo :: Finite n -> Finite n -> Finite n -> [Finite n] Source #
Generic (Finite n) Source #
Instance details Defined in Data.Finite.Internal Associated Types type Rep (Finite n) :: Type -> Type Source # Methods from :: Finite n -> Rep (Finite n) x Source # to :: Rep (Finite n) x -> Finite n Source #
KnownNat n => Num (Finite n) Source #	`+`, `-`, and `*` implement arithmetic modulo `n`. The `fromInteger` function raises an error for inputs outside of bounds.
Instance details Defined in Data.Finite.Internal Methods (+) :: Finite n -> Finite n -> Finite n Source # (-) :: Finite n -> Finite n -> Finite n Source # (*) :: Finite n -> Finite n -> Finite n Source # negate :: Finite n -> Finite n Source # abs :: Finite n -> Finite n Source # signum :: Finite n -> Finite n Source # fromInteger :: Integer -> Finite n Source #
KnownNat n => Read (Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods readsPrec :: Int -> ReadS (Finite n) Source # readList :: ReadS [Finite n] Source # readPrec :: ReadPrec (Finite n) Source # readListPrec :: ReadPrec [Finite n] Source #
KnownNat n => Integral (Finite n) Source #	`quot` and `rem` are the same as `div` and `mod` and they implement regular division of numbers in the range `[0, n)`, not modular arithmetic.
Instance details Defined in Data.Finite.Internal Methods quot :: Finite n -> Finite n -> Finite n Source # rem :: Finite n -> Finite n -> Finite n Source # div :: Finite n -> Finite n -> Finite n Source # mod :: Finite n -> Finite n -> Finite n Source # quotRem :: Finite n -> Finite n -> (Finite n, Finite n) Source # divMod :: Finite n -> Finite n -> (Finite n, Finite n) Source # toInteger :: Finite n -> Integer Source #
KnownNat n => Real (Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods toRational :: Finite n -> Rational Source #
Show (Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods showsPrec :: Int -> Finite n -> ShowS Source # show :: Finite n -> String Source # showList :: [Finite n] -> ShowS Source #
NFData (Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods rnf :: Finite n -> () Source #
Eq (Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods (==) :: Finite n -> Finite n -> Bool Source # (/=) :: Finite n -> Finite n -> Bool Source #
Ord (Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods compare :: Finite n -> Finite n -> Ordering Source # (<) :: Finite n -> Finite n -> Bool Source # (<=) :: Finite n -> Finite n -> Bool Source # (>) :: Finite n -> Finite n -> Bool Source # (>=) :: Finite n -> Finite n -> Bool Source # max :: Finite n -> Finite n -> Finite n Source # min :: Finite n -> Finite n -> Finite n Source #
type Rep (Finite n) Source #
Instance details Defined in Data.Finite.Internal type Rep (Finite n) = D1 ('MetaData "Finite" "Data.Finite.Internal" "finite-typelits-0.1.6.0-JhiiygZsyRs3chMHxwzVFo" 'True) (C1 ('MetaCons "Finite" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

finite :: KnownNat n => Integer -> Finite n Source #

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

getFinite :: Finite n -> Integer Source #

Convert a Finite into the corresponding Integer.