lean-peano-1.0.2.0: A maximally lazy, simple implementation of the Peano numbers with minimal dependencies.

Numeric.Peano.Typelevel

Description

Simple type-level Peano naturals.

Synopsis

# 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 n) <= 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 #

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