Safe Haskell	Safe-Inferred
Language	Haskell2010

ConCat.Nat

Description

Simple type-level, Peano-style (unary) natural numbers

Synopsis

data Nat
- = Z
- | S Nat
type Z = 'Z
type S = 'S
type family (a :: Nat) + (b :: Nat) :: Nat where ...
type family a - b :: Nat where ...
type family a * b :: Nat where ...
type family a ^ b :: Nat where ...
type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7
type N9 = S N8
type N10 = S N9
type N11 = S N10
type N12 = S N11
type N13 = S N12
type N14 = S N13
type N15 = S N14
type N16 = S N15
type N17 = S N16
type N18 = S N17
type N19 = S N18
type N20 = S N19
type N21 = S N20
type N22 = S N21
type N23 = S N22
type N24 = S N23
type N25 = S N24
type N26 = S N25
type N27 = S N26
type N28 = S N27
type N29 = S N28
type N30 = S N29
type N31 = S N30
type N32 = S N31

Documentation

data Nat Source #

Constructors

Z
S Nat

type Z = 'Z Source #

type S = 'S Source #

type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 Source #

Sum of type-level numbers

Equations

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

type family a - b :: Nat where ... infixl 6 Source #

Difference of type-level numbers

Equations

n - Z = n
(S n) - (S m) = n - m

type family a * b :: Nat where ... infixl 7 Source #

Product of type-level numbers

Equations

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

type family a ^ b :: Nat where ... infixr 8 Source #

Exponentiating type-level numbers

Equations

a ^ Z = S Z
a ^ (S b) = a * (a ^ b)

type N0 = Z Source #

type N1 = S N0 Source #

type N2 = S N1 Source #

type N3 = S N2 Source #

type N4 = S N3 Source #

type N5 = S N4 Source #

type N6 = S N5 Source #

type N7 = S N6 Source #

type N8 = S N7 Source #

type N9 = S N8 Source #

type N10 = S N9 Source #

type N11 = S N10 Source #

type N12 = S N11 Source #

type N13 = S N12 Source #

type N14 = S N13 Source #

type N15 = S N14 Source #

type N16 = S N15 Source #

type N17 = S N16 Source #

type N18 = S N17 Source #

type N19 = S N18 Source #

type N20 = S N19 Source #

type N21 = S N20 Source #

type N22 = S N21 Source #

type N23 = S N22 Source #

type N24 = S N23 Source #

type N25 = S N24 Source #

type N26 = S N25 Source #

type N27 = S N26 Source #

type N28 = S N27 Source #

type N29 = S N28 Source #

type N30 = S N29 Source #

type N31 = S N30 Source #

type N32 = S N31 Source #