Type.Data.Num.Unary

Documentation

data Unary

Representation name for unary type level numbers.

Instances

Representation Unary

Defined in Type.Data.Num.Unary

Methods

reifyIntegral :: Proxy Unary -> Integer -> (forall s. (Integer s, Repr s ~ Unary) => Proxy s -> a) -> a

unary :: Proxy n -> Proxy (Un n)

data Un x

Instances

Natural a => Show (Un a)

Defined in Type.Data.Num.Unary

Methods

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

Natural n => Integer (Un n)

Defined in Type.Data.Num.Unary

Associated Types

type Repr (Un n)

Methods

singleton :: Singleton (Un n)

type Repr (Un n)

Defined in Type.Data.Num.Unary

type Repr (Un n) = Unary

type (Un x) :*: (Un y)

Defined in Type.Data.Num.Unary

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

type (Un x) :+: (Un y)

Defined in Type.Data.Num.Unary

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

data Zero

Instances

Natural Zero

Defined in Type.Data.Num.Unary

Methods

switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f Zero

type FromUnary Zero

Defined in Type.Data.Num.Decimal.Number

type FromUnary Zero = Zero

type _x :*: Zero

Defined in Type.Data.Num.Unary

type _x :*: Zero = Zero

type x :+: Zero

Defined in Type.Data.Num.Unary

type x :+: Zero = x

data Succ x

Instances

Natural n => Positive (Succ n)

Defined in Type.Data.Num.Unary

Methods

switchPos :: (forall m. Natural m => f (Succ m)) -> f (Succ n)

Natural n => Natural (Succ n)

Defined in Type.Data.Num.Unary

Methods

switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f (Succ n)

type x :*: (Succ y)

Defined in Type.Data.Num.Unary

type x :*: (Succ y) = x :+: (x :*: y)

type x :+: (Succ y)

Defined in Type.Data.Num.Unary

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

type FromUnary (Succ n)

Defined in Type.Data.Num.Decimal.Number

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

zero :: Proxy Zero

succ :: Proxy n -> Proxy (Succ n)

data HeadSingleton n where

Constructors

Zero :: HeadSingleton Zero

Succ :: Natural n => HeadSingleton (Succ n)

headSingleton :: Natural n => HeadSingleton n

newtype Singleton n

Constructors

Singleton Integer

singleton :: Natural n => Singleton n

singletonFromProxy :: Natural n => Proxy n -> Singleton n

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

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

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

class Natural n where

Methods

switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f n

Instances

Natural Zero

Defined in Type.Data.Num.Unary

Methods

switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f Zero

Natural n => Natural (Succ n)

Defined in Type.Data.Num.Unary

Methods

switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f (Succ n)

class Natural n => Positive n where

Methods

switchPos :: (forall m. Natural m => f (Succ m)) -> f n

Instances

Natural n => Positive (Succ n)

Defined in Type.Data.Num.Unary

Methods

switchPos :: (forall m. Natural m => f (Succ m)) -> f (Succ n)

type family x :+: y

Instances

type x :+: Zero

Defined in Type.Data.Num.Unary

type x :+: Zero = x

type x :+: (Succ y)

Defined in Type.Data.Num.Unary

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

type family x :*: y

Instances

type _x :*: Zero

Defined in Type.Data.Num.Unary

type _x :*: Zero = Zero

type x :*: (Succ y)

Defined in Type.Data.Num.Unary

type x :*: (Succ y) = x :+: (x :*: y)

reifyNatural :: Integer -> (forall s. Natural s => Proxy s -> w) -> w