Safe Haskell	Safe
Language	Haskell2010

Numeric.Peano.Typelevel

Description

Simple type-level Peano naturals.

Synopsis

type family (n :: Nat) == (m :: Nat) :: Bool where ...
type family FromLit (n :: Nat) :: Nat where ...
type family ToLit (n :: Nat) :: Nat where ...
type family Compare (n :: Nat) (m :: Nat) :: Ordering where ...
type family (n :: Nat) <= (m :: Nat) :: Bool where ...
type family (n :: Nat) < (m :: Nat) :: Bool where ...
type family Min (n :: Nat) (m :: Nat) :: Nat where ...
type family Max (n :: Nat) (m :: Nat) :: Nat where ...
type family (n :: Nat) + (m :: Nat) :: Nat where ...
type family (n :: Nat) * (m :: Nat) :: Nat where ...
type family (n :: Nat) - (m :: Nat) :: Nat where ...
type family (n :: Nat) % (m :: Nat) :: Nat where ...
type family (n :: Nat) / (m :: Nat) :: Nat where ...

Documentation

type family (n :: Nat) == (m :: Nat) :: Bool where ... Source #

Equality of type-level naturals.

Equations

Z == Z = True
(S n) == (S m) = n == m
Z == (S _) = False
(S _) == Z = False

type family FromLit (n :: Nat) :: Nat where ... Source #

Conversion of numeric literals to naturals.

Equations

FromLit 0 = Z
FromLit n = S (FromLit (n - 1))

type family ToLit (n :: Nat) :: Nat where ... Source #

Conversion of naturals to numeric literals.

Equations

ToLit Z = 0
ToLit (S n) = 1 + ToLit n

type family Compare (n :: Nat) (m :: Nat) :: Ordering where ... Source #

Comparison of type-level naturals.

Equations

Compare Z Z = EQ
Compare (S n) (S m) = Compare n m
Compare Z (S _) = LT
Compare (S _) Z = GT

type family (n :: Nat) <= (m :: Nat) :: Bool where ... Source #

<= on type-level naturals.

Equations

Z <= _ = True
(S _) <= Z = False
(S n) <= (S m) = n <= m

type family (n :: Nat) < (m :: Nat) :: Bool where ... Source #

< on type-level naturals.

Equations

_ < Z = False
n < (S m) = n <= m

type family Min (n :: Nat) (m :: Nat) :: Nat where ... Source #

The minimum of two type-level naturals.

Equations

Min Z _ = Z
Min _ Z = Z
Min (S n) (S m) = S (Min n m)

type family Max (n :: Nat) (m :: Nat) :: Nat where ... Source #

The maximum of two type-level naturals.

Equations

Max Z m = m
Max n Z = n
Max (S n) (S m) = S (Max n m)

type family (n :: Nat) + (m :: Nat) :: Nat where ... infixl 6 Source #

Addition of type-level naturals.

Equations

Z + m = m
(S n) + m = S (n + m)

type family (n :: Nat) * (m :: Nat) :: Nat where ... infixl 7 Source #

Multiplication of type-level naturals.

Equations

Z * _ = Z
(S n) * m = m + (n * m)

type family (n :: Nat) - (m :: Nat) :: Nat where ... infixl 6 Source #

Subtraction of type-level naturals.

Equations

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

type family (n :: Nat) % (m :: Nat) :: Nat where ... Source #

Remainder on type-level naturals.

Equations

_ % Z = TypeError (Text "divide by zero")
n % m = Rem' n m n m

type family (n :: Nat) / (m :: Nat) :: Nat where ... Source #

Division on type-level naturals.

Equations

_ / Z = TypeError (Text "divide by zero")
n / m = Div' m n m