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

Safe HaskellSafe
LanguageHaskell2010

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 _) <= 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