Safe Haskell	Safe
Language	Haskell2010

Numeric.Peano.Typelevel

Documentation

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

Equations

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

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

Equations

FromLit 0 = Z
FromLit n = FromLit2 (Mod n 2) (FromLit (Div n 2))

type family FromLit2 (odd :: Nat) (rest :: Nat) :: Nat where ... Source #

Equations

FromLit2 0 n = n
FromLit2 1 n = S n

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

Equations

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

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

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 #

Equations

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

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

Equations

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

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

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 #

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 #

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

Rem' n m n' Z = Rem' n' m n' m
Rem' n m (S n') (S m') = Rem' n m n' m'
Rem' n m Z (S _) = n

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

Equations

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

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

Equations

Div' m n' Z = S (Div' m n' m)
Div' m (S n') (S m') = Div' m n' m'
Div' m Z (S _) = Z