type-fun-0.1.0: Collection of widely reimplemented type families

Safe Haskell	Safe
Language	Haskell2010

TypeFun.Data.Peano

Documentation

Constructors

Z
S N

Instances

Eq N Source
Ord N Source
Read N Source
Show N Source
Generic N Source
type Rep N Source

type family ToNat a :: Nat Source

Equations

ToNat Z = 0
ToNat (S a) = 1 + ToNat a

type family FromNat a :: N Source

Equations

FromNat 0 = Z
FromNat a = S (FromNat (a - 1))

type family a :+: b :: N Source

Equations

Z :+: b = b
(S a) :+: b = a :+: S b

type family a :-: b :: N Source

Equations

a :-: Z = a
(S a) :-: (S b) = a :-: b

type family a :*: b :: N Source

Equations

Z :*: b = Z
a :*: Z = Z
(S a) :: b = b :+: (a :: b)