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 #
Eq ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods (==) :: Finite n -> Finite n -> Bool Source # (/=) :: Finite n -> Finite n -> Bool 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 => 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 #
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 #
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 => 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 #
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 #
NFData ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods rnf :: 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-JWQ68Fc4Po0IMMqLp3mmi2" ' 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 .