Safe Haskell	Safe
Language	Haskell2010

Type.Data.Num.Decimal.Number

Synopsis

data Decimal
decimal :: Proxy n -> Proxy (Dec n)
data Dec x
data Zero
data Pos x xs
data Neg x xs
data EndAsc
data ds :< d
data EndDesc
data d :> ds
newtype Singleton x = Singleton Integer
singleton :: Integer x => Singleton x
singletonFromProxy :: Integer n => Proxy n -> Singleton n
integerFromSingleton :: Integer n => Singleton n -> Integer
integralFromSingleton :: (Integer n, Num a) => Singleton n -> a
integralFromProxy :: (Integer n, Num a) => Proxy n -> a
class Integer n where
class Integer n => Natural n where
class Natural n => Positive n where
class Integer n => Negative n where
reifyIntegral :: Integer -> (forall s. Integer s => Proxy s -> w) -> w
reifyNatural :: Integer -> (forall s. Natural s => Proxy s -> a) -> Maybe a
reifyPositive :: Integer -> (forall s. Positive s => Proxy s -> a) -> Maybe a
reifyNegative :: Integer -> (forall s. Negative s => Proxy s -> a) -> Maybe a
reifyPos :: Integer -> (forall x xs. (Pos x, Digits xs) => Proxy (Pos x xs) -> a) -> Maybe a
reifyNeg :: Integer -> (forall x xs. (Pos x, Digits xs) => Proxy (Neg x xs) -> a) -> Maybe a
class Digits xs where
type family x :+: y
type (:-:) x y = x :+: Negate y
type family x :*: y
type family Pred x
type family Succ x
type family Compare x y
type family IsEven x
type family Pow2 x
type family Log2Ceil x
class x :<: y
class x :<=: y
class x :==: y
class x :>: y
class x :>=: y
class x :/=: y
type family FromUnary n
type family ToUnary n
type family ToUnaryAcc m n
type UnaryAcc m x = ToUnary x :+: (m :*: U10)

Documentation

data Decimal #

Representation name for decimal type level numbers.

Instances

Representation Decimal #
Instance details Defined in Type.Data.Num.Decimal.Number Methods reifyIntegral :: Proxy Decimal -> Integer -> (forall s. (Integer s, Repr s ~ Decimal) => Proxy s -> a) -> a #
type One Decimal #
Instance details Defined in Type.Data.Num.Decimal.Number type One Decimal

decimal :: Proxy n -> Proxy (Dec n) #

data Dec x #

The wrapper type for decimal type level numbers.

Instances

Integer x => Integer (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number Associated Types type Repr (Dec x) :: * # Methods singleton :: Singleton (Dec x) #
x :/=: y => (Dec x) :/=: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :==: y => (Dec x) :==: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :>: y => (Dec x) :>: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :>=: y => (Dec x) :>=: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :<=: y => (Dec x) :<=: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :<: y => (Dec x) :<: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
type Repr (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type Repr (Dec x) = Decimal
type Log2Ceil (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type Log2Ceil (Dec x) = Dec (Log2Ceil x)
type Pow2 (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type Pow2 (Dec x) = Dec (Pow2 x)
type Div2 (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type Div2 (Dec x)
type Mul2 (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type Mul2 (Dec x) = Dec (x :+: x)
type IsEven (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type IsEven (Dec x) = IsEven x
type Pred (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type Pred (Dec x) = Dec (Pred x)
type Succ (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type Succ (Dec x) = Dec (Succ x)
type IsNatural (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type IsNatural (Dec x)
type IsNegative (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type IsNegative (Dec x)
type IsZero (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type IsZero (Dec x)
type IsPositive (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type IsPositive (Dec x)
type Negate (Dec x) #
Instance details Defined in Type.Data.Num.Decimal.Number type Negate (Dec x)
type (Dec x) :*: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Dec x) :: (Dec y) = Dec (x :: y)
type (Dec x) :-: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Dec x) :-: (Dec y) = Dec (x :-: y)
type (Dec x) :+: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Dec x) :+: (Dec y) = Dec (x :+: y)
type Compare (Dec x) (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Dec x) (Dec y) = Compare x y

data Zero #

Instances

Natural Zero #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchNat :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f Zero #
Integer Zero #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switch :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Neg x xs)) -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f Zero #
Zero :==: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :>=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :<=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :/=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :/=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :>: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :>=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :<=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :<: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :/=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :/=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
type ToUnary Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type ToUnary Zero = Zero
type Pow2 Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Pow2 Zero
type IsEven Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type IsEven Zero = True
type Pred Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Pred Zero = Neg Dec1 EndDesc
type Succ Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Succ Zero
type Compare Zero Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare Zero Zero = EQ
type Zero :*: _y #
Instance details Defined in Type.Data.Num.Decimal.Number type Zero :*: _y = Zero
type Zero :+: y #
Instance details Defined in Type.Data.Num.Decimal.Number type Zero :+: y = y
type Compare Zero (Pos _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare Zero (Pos _y _ys) = LT
type Compare Zero (Neg _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare Zero (Neg _y _ys) = GT
type Compare (Pos _x _xs) Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Pos _x _xs) Zero = GT
type Compare (Neg _x _xs) Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Neg _x _xs) Zero = LT
type (Pos _x _xs) :*: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos _x _xs) :*: Zero = Zero
type (Neg _x _xs) :*: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg _x _xs) :*: Zero = Zero
type (Pos x xs) :+: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :+: Zero = Pos x xs
type (Neg x xs) :+: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :+: Zero = Neg x xs

data Pos x xs #

Instances

Zero :/=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :<=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :<: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x, Digits xs) => Positive (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchPos :: (forall x0 xs0. (Pos0 x0, Digits xs0) => f (Pos x0 xs0)) -> f (Pos x xs) #
(Pos x, Digits xs) => Natural (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchNat :: f Zero -> (forall x0 xs0. (Pos0 x0, Digits xs0) => f (Pos x0 xs0)) -> f (Pos x xs) #
(Pos x, Digits xs) => Integer (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switch :: f Zero -> (forall x0 xs0. (Pos0 x0, Digits xs0) => f (Neg x0 xs0)) -> (forall x1 xs1. (Pos0 x1, Digits xs1) => f (Pos x1 xs1)) -> f (Pos x xs) #
(Pos x xs) :/=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
IsEQ (ComparePos x xs y ys) ~ False => (Pos x xs) :/=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :/=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :/=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ EQ => (Pos x xs) :==: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ GT => (Pos x xs) :>: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
GreaterPos y ys x xs ~ False => (Pos x xs) :>=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
GreaterPos x xs y ys ~ False => (Pos x xs) :<=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ LT => (Pos x xs) :<: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
type Compare Zero (Pos _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare Zero (Pos _y _ys) = LT
type ToUnary (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type ToUnary (Pos x xs) = ToUnaryAcc (ToUnary x) xs
type Log2Ceil (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Log2Ceil (Pos x xs)
type Pow2 (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Pow2 (Pos x xs)
type IsEven (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type IsEven (Pos x xs)
type Pred (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Pred (Pos x xs)
type Succ (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Succ (Pos x xs)
type Compare (Pos _x _xs) Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Pos _x _xs) Zero = GT
type (Pos _x _xs) :*: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos _x _xs) :*: Zero = Zero
type (Pos x xs) :+: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :+: Zero = Pos x xs
type Compare (Pos _x _xs) (Neg _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Pos _x _xs) (Neg _y _ys) = GT
type Compare (Pos x xs) (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Pos x xs) (Pos y ys)
type Compare (Neg _x _xs) (Pos _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Neg _x _xs) (Pos _y _ys) = LT
type (Pos x xs) :*: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :*: (Neg y ys)
type (Pos x xs) :*: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :*: (Pos y ys)
type (Neg x xs) :*: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :*: (Pos y ys)
type (Pos x xs) :+: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :+: (Pos y ys)
type (Pos x xs) :+: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :+: (Neg y ys)
type (Neg x xs) :+: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :+: (Pos y ys)

data Neg x xs #

Instances

Zero :/=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :>: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :>=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x, Digits xs) => Negative (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchNeg :: (forall x0 xs0. (Pos x0, Digits xs0) => f (Neg x0 xs0)) -> f (Neg x xs) #
(Pos x, Digits xs) => Integer (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switch :: f Zero -> (forall x0 xs0. (Pos x0, Digits xs0) => f (Neg x0 xs0)) -> (forall x1 xs1. (Pos x1, Digits xs1) => f (Pos x1 xs1)) -> f (Neg x xs) #
(Neg x xs) :/=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :/=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
IsEQ (ComparePos x xs y ys) ~ False => (Neg x xs) :/=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :/=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ EQ => (Neg x xs) :==: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ LT => (Neg x xs) :>: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
GreaterPos x xs y ys ~ False => (Neg x xs) :>=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
GreaterPos y ys x xs ~ False => (Neg x xs) :<=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ GT => (Neg x xs) :<: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
type Compare Zero (Neg _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare Zero (Neg _y _ys) = GT
type IsEven (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type IsEven (Neg x xs)
type Pred (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Pred (Neg x xs)
type Succ (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Succ (Neg x xs)
type Compare (Neg _x _xs) Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Neg _x _xs) Zero = LT
type (Neg _x _xs) :*: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg _x _xs) :*: Zero = Zero
type (Neg x xs) :+: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :+: Zero = Neg x xs
type Compare (Pos _x _xs) (Neg _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Pos _x _xs) (Neg _y _ys) = GT
type Compare (Neg _x _xs) (Pos _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Neg _x _xs) (Pos _y _ys) = LT
type Compare (Neg x xs) (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Neg x xs) (Neg y ys)
type (Pos x xs) :*: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :*: (Neg y ys)
type (Neg x xs) :*: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :*: (Pos y ys)
type (Neg x xs) :*: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :*: (Neg y ys)
type (Pos x xs) :+: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :+: (Neg y ys)
type (Neg x xs) :+: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :+: (Neg y ys)
type (Neg x xs) :+: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :+: (Pos y ys)

data EndAsc #

The terminator type for ascending decimal digit lists.

Instances

Show EndAsc #
Instance details Defined in Type.Data.Num.Decimal.Number Methods showsPrec :: Int -> EndAsc -> ShowS # show :: EndAsc -> String # showList :: [EndAsc] -> ShowS #

data ds :< d infixl 9 #

data EndDesc #

The terminator type for descending decimal digit lists.

Instances

Show EndDesc #
Instance details Defined in Type.Data.Num.Decimal.Number Methods showsPrec :: Int -> EndDesc -> ShowS # show :: EndDesc -> String # showList :: [EndDesc] -> ShowS #
Digits EndDesc #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchDigits :: f EndDesc -> (forall xh xl. (C xh, Digits xl) => f (xh :> xl)) -> f EndDesc #
type ToUnaryAcc m EndDesc #
Instance details Defined in Type.Data.Num.Decimal.Number type ToUnaryAcc m EndDesc = m

data d :> ds infixr 9 #

Instances

(C xh, Digits xl) => Digits (xh :> xl) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchDigits :: f EndDesc -> (forall xh0 xl0. (C xh0, Digits xl0) => f (xh0 :> xl0)) -> f (xh :> xl) #
type ToUnaryAcc m (x :> xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type ToUnaryAcc m (x :> xs) = ToUnaryAcc (UnaryAcc m x) xs

newtype Singleton x #

Constructors

Singleton Integer

singleton :: Integer x => Singleton x #

singletonFromProxy :: Integer n => Proxy n -> Singleton n #

integerFromSingleton :: Integer n => Singleton n -> Integer #

integralFromSingleton :: (Integer n, Num a) => Singleton n -> a #

integralFromProxy :: (Integer n, Num a) => Proxy n -> a #

class Integer n where #

Minimal complete definition

switch

Methods

switch :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Neg x xs)) -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n #

Instances

Integer Zero #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switch :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Neg x xs)) -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f Zero #
(Pos x, Digits xs) => Integer (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switch :: f Zero -> (forall x0 xs0. (Pos0 x0, Digits xs0) => f (Neg x0 xs0)) -> (forall x1 xs1. (Pos0 x1, Digits xs1) => f (Pos x1 xs1)) -> f (Pos x xs) #
(Pos x, Digits xs) => Integer (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switch :: f Zero -> (forall x0 xs0. (Pos x0, Digits xs0) => f (Neg x0 xs0)) -> (forall x1 xs1. (Pos x1, Digits xs1) => f (Pos x1 xs1)) -> f (Neg x xs) #

class Integer n => Natural n where #

Minimal complete definition

switchNat

Methods

switchNat :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n #

Instances

Natural Zero #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchNat :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f Zero #
(Pos x, Digits xs) => Natural (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchNat :: f Zero -> (forall x0 xs0. (Pos0 x0, Digits xs0) => f (Pos x0 xs0)) -> f (Pos x xs) #

class Natural n => Positive n where #

Minimal complete definition

switchPos

Methods

switchPos :: (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n #

Instances

(Pos x, Digits xs) => Positive (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchPos :: (forall x0 xs0. (Pos0 x0, Digits xs0) => f (Pos x0 xs0)) -> f (Pos x xs) #

class Integer n => Negative n where #

Minimal complete definition

switchNeg

Methods

switchNeg :: (forall x xs. (Pos x, Digits xs) => f (Neg x xs)) -> f n #

Instances

(Pos x, Digits xs) => Negative (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchNeg :: (forall x0 xs0. (Pos x0, Digits xs0) => f (Neg x0 xs0)) -> f (Neg x xs) #

reifyIntegral :: Integer -> (forall s. Integer s => Proxy s -> w) -> w #

reifyNatural :: Integer -> (forall s. Natural s => Proxy s -> a) -> Maybe a #

reifyPositive :: Integer -> (forall s. Positive s => Proxy s -> a) -> Maybe a #

reifyNegative :: Integer -> (forall s. Negative s => Proxy s -> a) -> Maybe a #

reifyPos :: Integer -> (forall x xs. (Pos x, Digits xs) => Proxy (Pos x xs) -> a) -> Maybe a #

reifyNeg :: Integer -> (forall x xs. (Pos x, Digits xs) => Proxy (Neg x xs) -> a) -> Maybe a #

class Digits xs where #

Minimal complete definition

switchDigits

Methods

switchDigits :: f EndDesc -> (forall xh xl. (C xh, Digits xl) => f (xh :> xl)) -> f xs #

Instances

Digits EndDesc #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchDigits :: f EndDesc -> (forall xh xl. (C xh, Digits xl) => f (xh :> xl)) -> f EndDesc #
(C xh, Digits xl) => Digits (xh :> xl) #
Instance details Defined in Type.Data.Num.Decimal.Number Methods switchDigits :: f EndDesc -> (forall xh0 xl0. (C xh0, Digits xl0) => f (xh0 :> xl0)) -> f (xh :> xl) #

type family x :+: y #

Instances

type Zero :+: y #
Instance details Defined in Type.Data.Num.Decimal.Number type Zero :+: y = y
type (Pos x xs) :+: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :+: Zero = Pos x xs
type (Neg x xs) :+: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :+: Zero = Neg x xs
type (Pos x xs) :+: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :+: (Pos y ys)
type (Pos x xs) :+: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :+: (Neg y ys)
type (Neg x xs) :+: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :+: (Neg y ys)
type (Neg x xs) :+: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :+: (Pos y ys)

type (:-:) x y = x :+: Negate y #

type family x :*: y #

Instances

type Zero :*: _y #
Instance details Defined in Type.Data.Num.Decimal.Number type Zero :*: _y = Zero
type (Pos _x _xs) :*: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos _x _xs) :*: Zero = Zero
type (Neg _x _xs) :*: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg _x _xs) :*: Zero = Zero
type (Pos x xs) :*: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :*: (Neg y ys)
type (Pos x xs) :*: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Pos x xs) :*: (Pos y ys)
type (Neg x xs) :*: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :*: (Pos y ys)
type (Neg x xs) :*: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type (Neg x xs) :*: (Neg y ys)

type family Pred x #

Instances

type Pred Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Pred Zero = Neg Dec1 EndDesc
type Pred (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Pred (Pos x xs)
type Pred (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Pred (Neg x xs)

type family Succ x #

Instances

type Succ Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Succ Zero
type Succ (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Succ (Pos x xs)
type Succ (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Succ (Neg x xs)

type family Compare x y #

Instances

type Compare Zero Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare Zero Zero = EQ
type Compare Zero (Pos _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare Zero (Pos _y _ys) = LT
type Compare Zero (Neg _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare Zero (Neg _y _ys) = GT
type Compare (Pos _x _xs) Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Pos _x _xs) Zero = GT
type Compare (Neg _x _xs) Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Neg _x _xs) Zero = LT
type Compare (Pos _x _xs) (Neg _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Pos _x _xs) (Neg _y _ys) = GT
type Compare (Pos x xs) (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Pos x xs) (Pos y ys)
type Compare (Neg _x _xs) (Pos _y _ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Neg _x _xs) (Pos _y _ys) = LT
type Compare (Neg x xs) (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number type Compare (Neg x xs) (Neg y ys)

type family IsEven x #

Instances

type IsEven Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type IsEven Zero = True
type IsEven (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type IsEven (Pos x xs)
type IsEven (Neg x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type IsEven (Neg x xs)

type family Pow2 x #

Instances

type Pow2 Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type Pow2 Zero
type Pow2 (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Pow2 (Pos x xs)

type family Log2Ceil x #

Instances

type Log2Ceil (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type Log2Ceil (Pos x xs)

class x :<: y #

Instances

Zero :<: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :<: y => (Dec x) :<: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ LT => (Pos x xs) :<: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ GT => (Neg x xs) :<: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number

class x :<=: y #

Instances

Zero :<=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :<=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :<=: y => (Dec x) :<=: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
GreaterPos x xs y ys ~ False => (Pos x xs) :<=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
GreaterPos y ys x xs ~ False => (Neg x xs) :<=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :<=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number

class x :==: y #

Instances

Zero :==: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
x :==: y => (Dec x) :==: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ EQ => (Pos x xs) :==: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ EQ => (Neg x xs) :==: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number

class x :>: y #

Instances

Zero :>: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :>: y => (Dec x) :>: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ GT => (Pos x xs) :>: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
ComparePos x xs y ys ~ LT => (Neg x xs) :>: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number

class x :>=: y #

Instances

Zero :>=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :>=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :>=: y => (Dec x) :>=: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
GreaterPos y ys x xs ~ False => (Pos x xs) :>=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :>=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
GreaterPos x xs y ys ~ False => (Neg x xs) :>=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number

class x :/=: y #

Instances

Zero :/=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
Zero :/=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
x :/=: y => (Dec x) :/=: (Dec y) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :/=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :/=: Zero #
Instance details Defined in Type.Data.Num.Decimal.Number
IsEQ (ComparePos x xs y ys) ~ False => (Pos x xs) :/=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Pos x xs) :/=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
IsEQ (ComparePos x xs y ys) ~ False => (Neg x xs) :/=: (Neg y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number
(Neg x xs) :/=: (Pos y ys) #
Instance details Defined in Type.Data.Num.Decimal.Number

type family FromUnary n #

Instances

type FromUnary Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type FromUnary Zero = Zero
type FromUnary (Succ n) #
Instance details Defined in Type.Data.Num.Decimal.Number type FromUnary (Succ n) = Succ (FromUnary n)

type family ToUnary n #

Instances

type ToUnary Zero #
Instance details Defined in Type.Data.Num.Decimal.Number type ToUnary Zero = Zero
type ToUnary (Pos x xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type ToUnary (Pos x xs) = ToUnaryAcc (ToUnary x) xs

type family ToUnaryAcc m n #

Instances

type ToUnaryAcc m EndDesc #
Instance details Defined in Type.Data.Num.Decimal.Number type ToUnaryAcc m EndDesc = m
type ToUnaryAcc m (x :> xs) #
Instance details Defined in Type.Data.Num.Decimal.Number type ToUnaryAcc m (x :> xs) = ToUnaryAcc (UnaryAcc m x) xs

type UnaryAcc m x = ToUnary x :+: (m :*: U10) #