Safe Haskell	Safe-Inferred
Language	Haskell2010

Math.Number.TypeRational

Documentation

data SNat Source #

Constructors

Ze
Su SNat
SNegate SNat

data SBin Source #

Constructors

SBZe
SBOne SBin
SBZero SBin

data Sing :: SNat -> * where Source #

Constructors

SNatZ :: Sing 'Ze
SNatS :: Sing s -> Sing ('Su s)

Instances

Instances details

SingInteger (Sing x) => SingInteger (Sing ('Su x)) Source #
Instance details Defined in Math.Number.TypeRational Methods singToInteger :: Sing ('Su x) -> Integer Source #
SingInteger (Sing 'Ze) Source #
Instance details Defined in Math.Number.TypeRational Methods singToInteger :: Sing 'Ze -> Integer Source #

type family Half (n :: SNat) = s | s -> n where ... Source #

Equations

Half 'Ze = 'Ze
Half ('Su ('Su z)) = 'Su (Half z)

type family SPlus (n :: SNat) (n' :: SNat) where ... Source #

Equations

SPlus 'Ze 'Ze = 'Ze
SPlus 'Ze a = a
SPlus ('Su x) a = 'Su (SPlus x a)
SPlus a ('SNegate b) = SMinus a b
SPlus ('SNegate a) b = SMinus b a

type family SMinus (n :: SNat) (n' :: SNat) where ... Source #

Equations

SMinus 'Ze 'Ze = 'Ze
SMinus d 'Ze = d
SMinus 'Ze d = 'SNegate d
SMinus ('Su d) ('Su d') = SMinus d d'
SMinus a ('SNegate b) = SPlus a b
SMinus ('SNegate a) b = 'SNegate (SPlus a b)

class SingInteger n where Source #

Methods

singToInteger :: n -> Integer Source #

Instances

Instances details

(SingInteger (Sing n), SingPrime p) => SingInteger (PrimePowerSing ('PrimePower p n)) Source #
Instance details Defined in Math.Number.TypeRational Methods singToInteger :: PrimePowerSing ('PrimePower p n) -> Integer Source #
SingPrime n => SingInteger (PrimeSing n) Source #
Instance details Defined in Math.Number.TypeRational Methods singToInteger :: PrimeSing n -> Integer Source #
SingInteger (Sing x) => SingInteger (Sing ('Su x)) Source #
Instance details Defined in Math.Number.TypeRational Methods singToInteger :: Sing ('Su x) -> Integer Source #
SingInteger (Sing 'Ze) Source #
Instance details Defined in Math.Number.TypeRational Methods singToInteger :: Sing 'Ze -> Integer Source #

class SingRational r where Source #

Methods

singToRational :: r -> Rational Source #

class SingPrime (n :: Prime) where Source #

Methods

singToPrimeIndex :: PrimeSing n -> Integer Source #

Instances

Instances details

SingPrime 'PrTwo Source #
Instance details Defined in Math.Number.TypeRational Methods singToPrimeIndex :: PrimeSing 'PrTwo -> Integer Source #
SingPrime p => SingPrime ('NextPrimeAfter p) Source #
Instance details Defined in Math.Number.TypeRational Methods singToPrimeIndex :: PrimeSing ('NextPrimeAfter p) -> Integer Source #

data PrimeSing :: Prime -> * where Source #

Constructors

SPrTwo :: PrimeSing 'PrTwo
SPrNext :: PrimeSing n -> PrimeSing ('NextPrimeAfter n)

Instances

Instances details

SingPrime n => SingInteger (PrimeSing n) Source #
Instance details Defined in Math.Number.TypeRational Methods singToInteger :: PrimeSing n -> Integer Source #

data PrimePowerSing :: PrimePower -> * where Source #

Constructors

SPrimePower :: PrimeSing p -> Sing n -> PrimePowerSing ('PrimePower p n)

Instances

Instances details

(SingInteger (Sing n), SingPrime p) => SingInteger (PrimePowerSing ('PrimePower p n)) Source #
Instance details Defined in Math.Number.TypeRational Methods singToInteger :: PrimePowerSing ('PrimePower p n) -> Integer Source #

data RatSing :: SRat -> * where Source #

Constructors

SRatOne :: RatSing 'PrOne
SRatTimes :: PrimePowerSing p -> RatSing r -> RatSing ('PrTimes p r)

data SRat Source #

Constructors

PrOne
PrTimes PrimePower SRat

data PrimePower Source #

Constructors

PrimePower Prime SNat

data Prime Source #

Constructors

PrTwo
NextPrimeAfter Prime

type family InvertPrime (a :: SRat) = (c :: SRat) | c -> a where ... Source #

Equations

InvertPrime 'PrOne = 'PrOne
InvertPrime ('PrTimes ('PrimePower p n) r) = 'PrTimes ('PrimePower p ('SNegate n)) (InvertPrime r)

type family ShiftPrime (a :: SRat) = (c :: SRat) | c -> a where ... Source #

Equations

ShiftPrime 'PrOne = 'PrTimes PPTwo 'PrOne
ShiftPrime ('PrTimes ('PrimePower p n) r) = 'PrTimes ('PrimePower ('NextPrimeAfter p) n) r

type family RatMul (a :: SRat) (b :: SRat) :: SRat where ... Source #

Equations

RatMul ('PrTimes ('PrimePower 'PrTwo n) r) ('PrTimes ('PrimePower 'PrTwo m) r') = 'PrTimes ('PrimePower 'PrTwo (SPlus n m)) (RatMul r r')
RatMul ('PrTimes ('PrimePower ('NextPrimeAfter p) n) r) ('PrTimes ('PrimePower ('NextPrimeAfter q) n') r') = ShiftPrime (RatMul ('PrTimes ('PrimePower p n) r) ('PrTimes ('PrimePower q n') r'))
RatMul ('PrTimes ('PrimePower 'PrTwo n) r) ('PrTimes ('PrimePower ('NextPrimeAfter p) m) r') = 'PrTimes ('PrimePower 'PrTwo n) (RatMul r ('PrTimes ('PrimePower ('NextPrimeAfter p) m) r'))
RatMul ('PrTimes ('PrimePower ('NextPrimeAfter p) n) r) ('PrTimes ('PrimePower 'PrTwo m) r') = 'PrTimes ('PrimePower 'PrTwo m) (RatMul ('PrTimes ('PrimePower ('NextPrimeAfter p) n) r) r')
RatMul 'PrOne ('PrTimes a b) = 'PrTimes a b
RatMul ('PrTimes a b) 'PrOne = 'PrTimes a b
RatMul 'PrOne 'PrOne = 'PrOne

type family RatDiv (a :: SRat) (b :: SRat) :: SRat where ... Source #

Equations

RatDiv ('PrTimes ('PrimePower 'PrTwo n) r) ('PrTimes ('PrimePower 'PrTwo m) r') = 'PrTimes ('PrimePower 'PrTwo (SMinus n m)) (RatDiv r r')
RatDiv ('PrTimes ('PrimePower ('NextPrimeAfter p) n) r) ('PrTimes ('PrimePower ('NextPrimeAfter q) n') r') = ShiftPrime (RatDiv ('PrTimes ('PrimePower p n) r) ('PrTimes ('PrimePower q n') r'))
RatDiv ('PrTimes ('PrimePower 'PrTwo n) r) ('PrTimes ('PrimePower ('NextPrimeAfter p) m) r') = 'PrTimes ('PrimePower 'PrTwo n) (RatDiv r ('PrTimes ('PrimePower ('NextPrimeAfter p) m) r'))
RatDiv ('PrTimes ('PrimePower ('NextPrimeAfter p) n) r) ('PrTimes ('PrimePower 'PrTwo m) r') = 'PrTimes ('PrimePower 'PrTwo m) (RatDiv ('PrTimes ('PrimePower ('NextPrimeAfter p) n) r) r')
RatDiv 'PrOne ('PrTimes a b) = InvertPrime ('PrTimes a b)
RatDiv ('PrTimes a b) 'PrOne = 'PrTimes a b
RatDiv 'PrOne 'PrOne = 'PrOne