finite-typelits-0.1.6.0: A type inhabited by finitely many values, indexed by type-level naturals
Copyright(C) 2015-2022 mniip
LicenseBSD3
Maintainermniip <mniip@mniip.com>
Stabilityexperimental
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Finite.Internal

Description

 
Synopsis

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 #

maxBound :: Finite n #

KnownNat n => Enum (Finite n) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Finite.Internal

Methods

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

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

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 #

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) 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 #

(-) :: 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) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Finite.Internal

KnownNat n => Real (Finite n) Source # 
Instance details

Defined in Data.Finite.Internal

Methods

toRational :: Finite n -> Rational #

Show (Finite n) Source # 
Instance details

Defined in Data.Finite.Internal

Methods

showsPrec :: Int -> Finite n -> ShowS #

show :: Finite n -> String #

showList :: [Finite n] -> ShowS #

Generic (Finite n) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Finite.Internal

Methods

rnf :: Finite n -> () #

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-7iT0U1QoBoT5NQD5AgM8KZ" '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.