Type.Data.Num.Decimal.Number

Documentation

data Decimal

Representation name for decimal type level numbers.

Instances

Representation Decimal

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

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 a => Show (Dec a)

Defined in Type.Data.Num.Decimal.Number

Methods

showsPrec :: Int -> Proxy (Dec a) -> ShowS

Integer x => Integer (Dec x)

Defined in Type.Data.Num.Decimal.Number

Associated Types

type Repr (Dec x)

Methods

singleton :: Singleton (Dec x)

x :/=: y => (Dec x) :/=: (Dec y)

Defined in Type.Data.Num.Decimal.Number

x :==: y => (Dec x) :==: (Dec y)

Defined in Type.Data.Num.Decimal.Number

x :>: y => (Dec x) :>: (Dec y)

Defined in Type.Data.Num.Decimal.Number

x :>=: y => (Dec x) :>=: (Dec y)

Defined in Type.Data.Num.Decimal.Number

x :<=: y => (Dec x) :<=: (Dec y)

Defined in Type.Data.Num.Decimal.Number

x :<: y => (Dec x) :<: (Dec y)

Defined in Type.Data.Num.Decimal.Number

type Repr (Dec x)

Defined in Type.Data.Num.Decimal.Number

type Repr (Dec x) = Decimal

type Log2Ceil (Dec x)

Defined in Type.Data.Num.Decimal.Number

type Log2Ceil (Dec x) = Dec (Log2Ceil x)

type Pow2 (Dec x)

Defined in Type.Data.Num.Decimal.Number

type Pow2 (Dec x) = Dec (Pow2 x)

type Div2 (Dec x)

Defined in Type.Data.Num.Decimal.Number

type Div2 (Dec x)

type Mul2 (Dec x)

Defined in Type.Data.Num.Decimal.Number

type Mul2 (Dec x) = Dec (x :+: x)

type IsEven (Dec x)

Defined in Type.Data.Num.Decimal.Number

type IsEven (Dec x) = IsEven x

type Pred (Dec x)

Defined in Type.Data.Num.Decimal.Number

type Pred (Dec x) = Dec (Pred x)

type Succ (Dec x)

Defined in Type.Data.Num.Decimal.Number

type Succ (Dec x) = Dec (Succ x)

type IsNatural (Dec x)

Defined in Type.Data.Num.Decimal.Number

type IsNatural (Dec x)

type IsNegative (Dec x)

Defined in Type.Data.Num.Decimal.Number

type IsNegative (Dec x)

type IsZero (Dec x)

Defined in Type.Data.Num.Decimal.Number

type IsZero (Dec x)

type IsPositive (Dec x)

Defined in Type.Data.Num.Decimal.Number

type IsPositive (Dec x)

type Negate (Dec x)

Defined in Type.Data.Num.Decimal.Number

type Negate (Dec x)

type (Dec x) :*: (Dec y)

Defined in Type.Data.Num.Decimal.Number

type (Dec x) :*: (Dec y) = Dec (x :*: y)

type (Dec x) :-: (Dec y)

Defined in Type.Data.Num.Decimal.Number

type (Dec x) :-: (Dec y) = Dec (x :-: y)

type (Dec x) :+: (Dec y)

Defined in Type.Data.Num.Decimal.Number

type (Dec x) :+: (Dec y) = Dec (x :+: y)

type Compare (Dec x) (Dec y)

Defined in Type.Data.Num.Decimal.Number

type Compare (Dec x) (Dec y) = Compare x y

data Zero

Instances

Natural Zero

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

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

Defined in Type.Data.Num.Decimal.Number

Zero :>=: Zero

Defined in Type.Data.Num.Decimal.Number

Zero :<=: Zero

Defined in Type.Data.Num.Decimal.Number

Zero :/=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :/=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :>: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :>=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :<=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :<: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :/=: Zero

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :/=: Zero

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>: Zero

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>=: Zero

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<=: Zero

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<: Zero

Defined in Type.Data.Num.Decimal.Number

type ToUnary Zero

Defined in Type.Data.Num.Decimal.Number

type ToUnary Zero = Zero

type Pow2 Zero

Defined in Type.Data.Num.Decimal.Number

type Pow2 Zero

type IsEven Zero

Defined in Type.Data.Num.Decimal.Number

type IsEven Zero = True

type Pred Zero

Defined in Type.Data.Num.Decimal.Number

type Pred Zero = Neg Dec1 EndDesc

type Succ Zero

Defined in Type.Data.Num.Decimal.Number

type Succ Zero

type Compare Zero Zero

Defined in Type.Data.Num.Decimal.Number

type Compare Zero Zero = EQ

type Zero :*: _y

Defined in Type.Data.Num.Decimal.Number

type Zero :*: _y = Zero

type Zero :+: y

Defined in Type.Data.Num.Decimal.Number

type Zero :+: y = y

type Compare Zero (Pos _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare Zero (Pos _y _ys) = LT

type Compare Zero (Neg _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare Zero (Neg _y _ys) = GT

type Compare (Pos _x _xs) Zero

Defined in Type.Data.Num.Decimal.Number

type Compare (Pos _x _xs) Zero = GT

type Compare (Neg _x _xs) Zero

Defined in Type.Data.Num.Decimal.Number

type Compare (Neg _x _xs) Zero = LT

type (Pos _x _xs) :*: Zero

Defined in Type.Data.Num.Decimal.Number

type (Pos _x _xs) :*: Zero = Zero

type (Neg _x _xs) :*: Zero

Defined in Type.Data.Num.Decimal.Number

type (Neg _x _xs) :*: Zero = Zero

type (Pos x xs) :+: Zero

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :+: Zero = Pos x xs

type (Neg x xs) :+: Zero

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :+: Zero = Neg x xs

data Pos x xs

Instances

Zero :/=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :<=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :<: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x, Digits xs) => Positive (Pos x xs)

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)

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)

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

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>: Zero

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>=: Zero

Defined in Type.Data.Num.Decimal.Number

IsEQ (ComparePos x xs y ys) ~ False => (Pos x xs) :/=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :/=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :/=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ EQ => (Pos x xs) :==: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ GT => (Pos x xs) :>: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

GreaterPos y ys x xs ~ False => (Pos x xs) :>=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

GreaterPos x xs y ys ~ False => (Pos x xs) :<=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ LT => (Pos x xs) :<: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type Compare Zero (Pos _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare Zero (Pos _y _ys) = LT

type ToUnary (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type ToUnary (Pos x xs) = ToUnaryAcc (ToUnary x) xs

type Log2Ceil (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type Log2Ceil (Pos x xs)

type Pow2 (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type Pow2 (Pos x xs)

type IsEven (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type IsEven (Pos x xs)

type Pred (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type Pred (Pos x xs)

type Succ (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type Succ (Pos x xs)

type Compare (Pos _x _xs) Zero

Defined in Type.Data.Num.Decimal.Number

type Compare (Pos _x _xs) Zero = GT

type (Pos _x _xs) :*: Zero

Defined in Type.Data.Num.Decimal.Number

type (Pos _x _xs) :*: Zero = Zero

type (Pos x xs) :+: Zero

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :+: Zero = Pos x xs

type Compare (Pos _x _xs) (Neg _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Pos _x _xs) (Neg _y _ys) = GT

type Compare (Pos x xs) (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Pos x xs) (Pos y ys)

type Compare (Neg _x _xs) (Pos _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Neg _x _xs) (Pos _y _ys) = LT

type (Pos x xs) :*: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :*: (Neg y ys)

type (Pos x xs) :*: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :*: (Pos y ys)

type (Neg x xs) :*: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :*: (Pos y ys)

type (Pos x xs) :+: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :+: (Pos y ys)

type (Pos x xs) :+: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :+: (Neg y ys)

type (Neg x xs) :+: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :+: (Pos y ys)

data Neg x xs

Instances

Zero :/=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :>: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :>=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x, Digits xs) => Negative (Neg x xs)

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)

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

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<=: Zero

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<: Zero

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :/=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

IsEQ (ComparePos x xs y ys) ~ False => (Neg x xs) :/=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :/=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ EQ => (Neg x xs) :==: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ LT => (Neg x xs) :>: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

GreaterPos x xs y ys ~ False => (Neg x xs) :>=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

GreaterPos y ys x xs ~ False => (Neg x xs) :<=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ GT => (Neg x xs) :<: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type Compare Zero (Neg _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare Zero (Neg _y _ys) = GT

type IsEven (Neg x xs)

Defined in Type.Data.Num.Decimal.Number

type IsEven (Neg x xs)

type Pred (Neg x xs)

Defined in Type.Data.Num.Decimal.Number

type Pred (Neg x xs)

type Succ (Neg x xs)

Defined in Type.Data.Num.Decimal.Number

type Succ (Neg x xs)

type Compare (Neg _x _xs) Zero

Defined in Type.Data.Num.Decimal.Number

type Compare (Neg _x _xs) Zero = LT

type (Neg _x _xs) :*: Zero

Defined in Type.Data.Num.Decimal.Number

type (Neg _x _xs) :*: Zero = Zero

type (Neg x xs) :+: Zero

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :+: Zero = Neg x xs

type Compare (Pos _x _xs) (Neg _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Pos _x _xs) (Neg _y _ys) = GT

type Compare (Neg _x _xs) (Pos _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Neg _x _xs) (Pos _y _ys) = LT

type Compare (Neg x xs) (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Neg x xs) (Neg y ys)

type (Pos x xs) :*: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :*: (Neg y ys)

type (Neg x xs) :*: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :*: (Pos y ys)

type (Neg x xs) :*: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :*: (Neg y ys)

type (Pos x xs) :+: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :+: (Neg y ys)

type (Neg x xs) :+: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :+: (Neg y ys)

type (Neg x xs) :+: (Pos y ys)

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

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

Defined in Type.Data.Num.Decimal.Number

Methods

showsPrec :: Int -> EndDesc -> ShowS

show :: EndDesc -> String

showList :: [EndDesc] -> ShowS

Digits EndDesc

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

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)

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)

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

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

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)

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)

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

Methods

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

Instances

Natural Zero

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)

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

Methods

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

Instances

(Pos x, Digits xs) => Positive (Pos x xs)

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

Methods

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

Instances

(Pos x, Digits xs) => Negative (Neg x xs)

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

Methods

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

Instances

Digits EndDesc

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)

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

Defined in Type.Data.Num.Decimal.Number

type Zero :+: y = y

type (Pos x xs) :+: Zero

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :+: Zero = Pos x xs

type (Neg x xs) :+: Zero

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :+: Zero = Neg x xs

type (Pos x xs) :+: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :+: (Pos y ys)

type (Pos x xs) :+: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :+: (Neg y ys)

type (Neg x xs) :+: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :+: (Neg y ys)

type (Neg x xs) :+: (Pos y ys)

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

Defined in Type.Data.Num.Decimal.Number

type Zero :*: _y = Zero

type (Pos _x _xs) :*: Zero

Defined in Type.Data.Num.Decimal.Number

type (Pos _x _xs) :*: Zero = Zero

type (Neg _x _xs) :*: Zero

Defined in Type.Data.Num.Decimal.Number

type (Neg _x _xs) :*: Zero = Zero

type (Pos x xs) :*: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :*: (Neg y ys)

type (Pos x xs) :*: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type (Pos x xs) :*: (Pos y ys)

type (Neg x xs) :*: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :*: (Pos y ys)

type (Neg x xs) :*: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type (Neg x xs) :*: (Neg y ys)

type family Pred x

Instances

type Pred Zero

Defined in Type.Data.Num.Decimal.Number

type Pred Zero = Neg Dec1 EndDesc

type Pred (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type Pred (Pos x xs)

type Pred (Neg x xs)

Defined in Type.Data.Num.Decimal.Number

type Pred (Neg x xs)

type family Succ x

Instances

type Succ Zero

Defined in Type.Data.Num.Decimal.Number

type Succ Zero

type Succ (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type Succ (Pos x xs)

type Succ (Neg x xs)

Defined in Type.Data.Num.Decimal.Number

type Succ (Neg x xs)

type family Compare x y

Instances

type Compare Zero Zero

Defined in Type.Data.Num.Decimal.Number

type Compare Zero Zero = EQ

type Compare Zero (Pos _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare Zero (Pos _y _ys) = LT

type Compare Zero (Neg _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare Zero (Neg _y _ys) = GT

type Compare (Pos _x _xs) Zero

Defined in Type.Data.Num.Decimal.Number

type Compare (Pos _x _xs) Zero = GT

type Compare (Neg _x _xs) Zero

Defined in Type.Data.Num.Decimal.Number

type Compare (Neg _x _xs) Zero = LT

type Compare (Pos _x _xs) (Neg _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Pos _x _xs) (Neg _y _ys) = GT

type Compare (Pos x xs) (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Pos x xs) (Pos y ys)

type Compare (Neg _x _xs) (Pos _y _ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Neg _x _xs) (Pos _y _ys) = LT

type Compare (Neg x xs) (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

type Compare (Neg x xs) (Neg y ys)

type family IsEven x

Instances

type IsEven Zero

Defined in Type.Data.Num.Decimal.Number

type IsEven Zero = True

type IsEven (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type IsEven (Pos x xs)

type IsEven (Neg x xs)

Defined in Type.Data.Num.Decimal.Number

type IsEven (Neg x xs)

type family Pow2 x

Instances

type Pow2 Zero

Defined in Type.Data.Num.Decimal.Number

type Pow2 Zero

type Pow2 (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type Pow2 (Pos x xs)

type family Log2Ceil x

Instances

type Log2Ceil (Pos x xs)

Defined in Type.Data.Num.Decimal.Number

type Log2Ceil (Pos x xs)

class x :<: y

Instances

Zero :<: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

x :<: y => (Dec x) :<: (Dec y)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<: Zero

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ LT => (Pos x xs) :<: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ GT => (Neg x xs) :<: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

class x :<=: y

Instances

Zero :<=: Zero

Defined in Type.Data.Num.Decimal.Number

Zero :<=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

x :<=: y => (Dec x) :<=: (Dec y)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<=: Zero

Defined in Type.Data.Num.Decimal.Number

GreaterPos x xs y ys ~ False => (Pos x xs) :<=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

GreaterPos y ys x xs ~ False => (Neg x xs) :<=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :<=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

class x :==: y

Instances

Zero :==: Zero

Defined in Type.Data.Num.Decimal.Number

x :==: y => (Dec x) :==: (Dec y)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ EQ => (Pos x xs) :==: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ EQ => (Neg x xs) :==: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

class x :>: y

Instances

Zero :>: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

x :>: y => (Dec x) :>: (Dec y)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>: Zero

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ GT => (Pos x xs) :>: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

ComparePos x xs y ys ~ LT => (Neg x xs) :>: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

class x :>=: y

Instances

Zero :>=: Zero

Defined in Type.Data.Num.Decimal.Number

Zero :>=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

x :>=: y => (Dec x) :>=: (Dec y)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>=: Zero

Defined in Type.Data.Num.Decimal.Number

GreaterPos y ys x xs ~ False => (Pos x xs) :>=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :>=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

GreaterPos x xs y ys ~ False => (Neg x xs) :>=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

class x :/=: y

Instances

Zero :/=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

Zero :/=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

x :/=: y => (Dec x) :/=: (Dec y)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :/=: Zero

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :/=: Zero

Defined in Type.Data.Num.Decimal.Number

IsEQ (ComparePos x xs y ys) ~ False => (Pos x xs) :/=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

(Pos x xs) :/=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

IsEQ (ComparePos x xs y ys) ~ False => (Neg x xs) :/=: (Neg y ys)

Defined in Type.Data.Num.Decimal.Number

(Neg x xs) :/=: (Pos y ys)

Defined in Type.Data.Num.Decimal.Number

type family FromUnary n

Instances

type FromUnary Zero

Defined in Type.Data.Num.Decimal.Number

type FromUnary Zero = Zero

type FromUnary (Succ n)

Defined in Type.Data.Num.Decimal.Number

type FromUnary (Succ n) = Succ (FromUnary n)

type family ToUnary n

Instances

type ToUnary Zero

Defined in Type.Data.Num.Decimal.Number

type ToUnary Zero = Zero

type ToUnary (Pos x xs)

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

Defined in Type.Data.Num.Decimal.Number

type ToUnaryAcc m EndDesc = m

type ToUnaryAcc m (x :> xs)

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)