Data.Nat

Nat :: *

Inductive natural numbers in Church-encoded style (Zero and Successor).

Implementation

data Nat = Zero | Succ Nat

plus :: Nat -> Nat -> Nat

Addition of two natural numbers via Church induction.

Implementation

plus m n = case m of
    Zero   -> n
    Succ p -> Succ p

mult :: Nat -> Nat -> Nat

Multiplication of two natural numbers via repeated addition.

Implementation

mult m n = case m of
    Zero   -> Zero
    Succ p -> plus n p

fold :: Nat -> (Nat -> B -> B) -> B -> B

The Church eliminator for natural numbers.

Implementation

fold n f z = case n of
    Zero   -> z
    Succ p -> f p

is_zero :: Nat -> Bool

Returns True if the number is Zero.

Implementation

is_zero n = case n of
    Zero   -> True
    Succ p -> False