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

Copyright(C) 2015 mniip
LicenseBSD3
Maintainermniip <mniip@mniip.com>
Stabilityexperimental
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Data.Finite.Internal

Description

 

Synopsis

Documentation

newtype Finite n Source #

Finite number type. Finite n is inhabited by exactly n values. Invariants:

getFinite x < natVal x
getFinite x >= 0

Constructors

Finite Integer 

Instances

KnownNat n => Bounded (Finite n) Source #

Throws an error for Finite 0

Methods

minBound :: Finite n #

maxBound :: Finite n #

KnownNat n => Enum (Finite n) Source # 

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 # 

Methods

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

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

KnownNat n => Integral (Finite n) Source # 

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 #

Modulo arithmetic. Only the fromInteger function is supposed to be useful.

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 # 

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 # 
KnownNat n => Real (Finite n) Source # 

Methods

toRational :: Finite n -> Rational #

Show (Finite n) Source # 

Methods

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

show :: Finite n -> String #

showList :: [Finite n] -> ShowS #

Generic (Finite n) Source # 

Associated Types

type Rep (Finite n) :: * -> * #

Methods

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

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

NFData (Finite n) Source # 

Methods

rnf :: Finite n -> () #

type Rep (Finite n) Source # 
type Rep (Finite n) = D1 (MetaData "Finite" "Data.Finite.Internal" "finite-typelits-0.1.3.0-3IB9vwQKJS8RiaHvY0GBC" True) (C1 (MetaCons "Finite" PrefixI False) (S1 (MetaSel (Nothing 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.