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

Safe Haskell	Safe
Language	Haskell2010

Type.Data.Num.Unary

Synopsis

Documentation

data Unary Source

Representation name for unary type level numbers.

Instances

Representation Unary Source

data Un x Source

Instances

Natural n => Integer (Un n) Source
type Repr (Un n) = Unary Source
type (Un x) :: (Un y) = Un ((::) x y) Source
type (Un x) :+: (Un y) = Un ((:+:) x y) Source

data Zero Source

Instances

Natural Zero Source
type FromUnary Zero = Zero Source
type _x :*: Zero = Zero Source
type x :+: Zero = x Source

data Succ x Source

Instances

Natural n => Positive (Succ n) Source
Natural n => Natural (Succ n) Source
type x :: (Succ y) = (:+:) x ((::) x y) Source
type x :+: (Succ y) = Succ ((:+:) x y) Source
type FromUnary (Succ n) = Succ (FromUnary n) Source

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

class Natural n where Source

Methods

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

Instances

Natural Zero Source
Natural n => Natural (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

type family x :+: y Source

Instances

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

type family x :*: y Source

Instances

type _x :*: Zero = Zero Source
type x :: (Succ y) = (:+:) x ((::) x y) Source