tfp-1.0.1: Type-level integers, booleans, lists using type families

Safe HaskellSafe
LanguageHaskell2010

Type.Data.Num.Unary

Synopsis

Documentation

data Unary Source #

Representation name for unary type level numbers.

Instances
Representation Unary Source # 
Instance details

Defined in Type.Data.Num.Unary

Methods

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

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

data Un x Source #

Instances
Natural a => Show (Un a) Source # 
Instance details

Defined in Type.Data.Num.Unary

Methods

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

Natural n => Integer (Un n) Source # 
Instance details

Defined in Type.Data.Num.Unary

Associated Types

type Repr (Un n) :: Type Source #

Methods

singleton :: Singleton (Un n) Source #

type Repr (Un n) Source # 
Instance details

Defined in Type.Data.Num.Unary

type Repr (Un n) = Unary
type (Un x) :*: (Un y) Source # 
Instance details

Defined in Type.Data.Num.Unary

type (Un x) :*: (Un y) = Un (x :*: y)
type (Un x) :+: (Un y) Source # 
Instance details

Defined in Type.Data.Num.Unary

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

data Zero Source #

Instances
Natural Zero Source # 
Instance details

Defined in Type.Data.Num.Unary

Methods

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

type FromUnary Zero Source # 
Instance details

Defined in Type.Data.Num.Decimal.Number

type FromUnary Zero = Zero
type _x :*: Zero Source # 
Instance details

Defined in Type.Data.Num.Unary

type _x :*: Zero = Zero
type x :+: Zero Source # 
Instance details

Defined in Type.Data.Num.Unary

type x :+: Zero = x

data Succ x Source #

Instances
Natural n => Positive (Succ n) Source # 
Instance details

Defined in Type.Data.Num.Unary

Methods

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

Natural n => Natural (Succ n) Source # 
Instance details

Defined in Type.Data.Num.Unary

Methods

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

type x :*: (Succ y) Source # 
Instance details

Defined in Type.Data.Num.Unary

type x :*: (Succ y) = x :+: (x :*: y)
type x :+: (Succ y) Source # 
Instance details

Defined in Type.Data.Num.Unary

type x :+: (Succ y) = Succ (x :+: y)
type FromUnary (Succ n) Source # 
Instance details

Defined in Type.Data.Num.Decimal.Number

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

zero :: Proxy Zero Source #

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

newtype Singleton n Source #

Constructors

Singleton Integer 

singleton :: Natural n => Singleton n Source #

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

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

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

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

class Natural n where Source #

Methods

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

Instances
Natural Zero Source # 
Instance details

Defined in Type.Data.Num.Unary

Methods

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

Natural n => Natural (Succ n) Source # 
Instance details

Defined in Type.Data.Num.Unary

Methods

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

class Natural n => Positive n where Source #

Methods

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

Instances
Natural n => Positive (Succ n) Source # 
Instance details

Defined in Type.Data.Num.Unary

Methods

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

type family x :+: y Source #

Instances
type x :+: Zero Source # 
Instance details

Defined in Type.Data.Num.Unary

type x :+: Zero = x
type x :+: (Succ y) Source # 
Instance details

Defined in Type.Data.Num.Unary

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

type family x :*: y Source #

Instances
type _x :*: Zero Source # 
Instance details

Defined in Type.Data.Num.Unary

type _x :*: Zero = Zero
type x :*: (Succ y) Source # 
Instance details

Defined in Type.Data.Num.Unary

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

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