Data.Finite.Internal

Documentation

newtype Finite (n :: Nat)

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

KnownNat n => Bounded (Finite n)

Throws an error for Finite 0

Defined in Data.Finite.Internal

Methods

minBound :: Finite n

maxBound :: Finite n

KnownNat n => Enum (Finite n)

Defined in Data.Finite.Internal

Methods

succ :: Finite n -> Finite n

pred :: Finite n -> Finite n

toEnum :: Int -> Finite n

fromEnum :: Finite n -> Int

enumFrom :: Finite n -> [Finite n]

enumFromThen :: Finite n -> Finite n -> [Finite n]

enumFromTo :: Finite n -> Finite n -> [Finite n]

enumFromThenTo :: Finite n -> Finite n -> Finite n -> [Finite n]

Eq (Finite n)

Defined in Data.Finite.Internal

Methods

(==) :: Finite n -> Finite n -> Bool

(/=) :: Finite n -> Finite n -> Bool

KnownNat n => Integral (Finite n)

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.

Defined in Data.Finite.Internal

Methods

quot :: Finite n -> Finite n -> Finite n

rem :: Finite n -> Finite n -> Finite n

div :: Finite n -> Finite n -> Finite n

mod :: Finite n -> Finite n -> Finite n

quotRem :: Finite n -> Finite n -> (Finite n, Finite n)

divMod :: Finite n -> Finite n -> (Finite n, Finite n)

toInteger :: Finite n -> Integer

KnownNat n => Num (Finite n)

+, -, and * implement arithmetic modulo n. The fromInteger function raises an error for inputs outside of bounds.

Defined in Data.Finite.Internal

Methods

(+) :: Finite n -> Finite n -> Finite n

(-) :: Finite n -> Finite n -> Finite n

(*) :: Finite n -> Finite n -> Finite n

negate :: Finite n -> Finite n

abs :: Finite n -> Finite n

signum :: Finite n -> Finite n

fromInteger :: Integer -> Finite n

Ord (Finite n)

Defined in Data.Finite.Internal

Methods

compare :: Finite n -> Finite n -> Ordering

(<) :: Finite n -> Finite n -> Bool

(<=) :: Finite n -> Finite n -> Bool

(>) :: Finite n -> Finite n -> Bool

(>=) :: Finite n -> Finite n -> Bool

max :: Finite n -> Finite n -> Finite n

min :: Finite n -> Finite n -> Finite n

KnownNat n => Read (Finite n)

Defined in Data.Finite.Internal

Methods

readsPrec :: Int -> ReadS (Finite n)

readList :: ReadS [Finite n]

readPrec :: ReadPrec (Finite n)

readListPrec :: ReadPrec [Finite n]

KnownNat n => Real (Finite n)

Defined in Data.Finite.Internal

Methods

toRational :: Finite n -> Rational

Show (Finite n)

Defined in Data.Finite.Internal

Methods

showsPrec :: Int -> Finite n -> ShowS

show :: Finite n -> String

showList :: [Finite n] -> ShowS

Generic (Finite n)

Defined in Data.Finite.Internal

Associated Types

type Rep (Finite n) :: Type -> Type

Methods

from :: Finite n -> Rep (Finite n) x

to :: Rep (Finite n) x -> Finite n

NFData (Finite n)

Defined in Data.Finite.Internal

Methods

rnf :: Finite n -> ()

type Rep (Finite n)

Defined in Data.Finite.Internal

type Rep (Finite n) = D1 ('MetaData "Finite" "Data.Finite.Internal" "finite-typelits-0.1.5.0-FVgX4hMFRt7L3G4cgHjFWv" 'True) (C1 ('MetaCons "Finite" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

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

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

getFinite :: Finite n -> Integer

Convert a Finite into the corresponding Integer.