Safe Haskell	Safe
Language	Haskell2010

Type.Data.Num.Unary

Synopsis

Documentation

Representation name for unary type level numbers.

Instances

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

data Un x #

Instances

Natural n => Integer (Un n) #
Associated Types type Repr (Un n) :: * # Methods singleton :: Singleton (Un n) #
type Repr (Un n) #
type Repr (Un n) = Unary
type (Un x) :*: (Un y) #
type (Un x) :: (Un y) = Un ((::) x y)
type (Un x) :+: (Un y) #
type (Un x) :+: (Un y) = Un ((:+:) x y)

data Zero #

Instances

Natural Zero #
Methods switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f Zero #
type FromUnary Zero #
type FromUnary Zero = Zero
type _x :*: Zero #
type _x :*: Zero = Zero
type x :+: Zero #
type x :+: Zero = x

data Succ x #

Instances

Natural n => Positive (Succ n) #
Methods switchPos :: (forall m. Natural m => f (Succ m)) -> f (Succ n) #
Natural n => Natural (Succ n) #
Methods switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f (Succ n) #
type x :*: (Succ y) #
type x :: (Succ y) = (:+:) x ((::) x y)
type x :+: (Succ y) #
type x :+: (Succ y) = Succ ((:+:) x y)
type FromUnary (Succ n) #
type FromUnary (Succ n) = Succ (FromUnary n)

newtype Singleton n #

Constructors

class Natural n where #

Minimal complete definition

Methods

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

Instances

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

class Natural n => Positive n where #

Minimal complete definition

Methods

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

Instances

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

type family x :+: y #

Instances

type family x :*: y #

Instances