-- Peano naturals
data Nat where
  Zero : Nat
  Succ : Nat -> Nat

-- Returns 10_000
main = toInt (fromInt 10000)

-- Peano arithmetic --

-- Peano addition
add : Nat -> Nat -> Nat
add left right = case left of
    Zero => right
    Succ n => Succ (add n right)

-- Peano multiplication
mul : Nat -> Nat -> Nat
mul left right = case right of
    Zero => Zero
    Succ n => add left (mul left n)

eq : Nat -> Nat -> Nat
eq a b = case a of
    Zero => case b of 
        Zero => Succ Zero
        _    => Zero
    Succ n => case b of
        Zero => Zero
        Succ m => eq n m

less : Nat -> Nat -> Nat
less a b = case a of
    Zero => case b of
        Zero => Zero
        Succ n => Succ Zero
    Succ n => case b of
        Zero => Zero
        Succ m => less n m

greater : Nat -> Nat -> Nat
greater a b = case b of
    Zero => case a of
        Zero => Zero
        Succ n => Succ Zero
    Succ n => case a of
        Zero => Zero
        Succ m => less n m

-- Aux

toInt : Nat -> Int
toInt a = case a of
    Succ n => 1 + toInt n
    Zero => 0

fromInt a = case a of
    0 => Zero
    n => Succ (fromInt (a - 1))