59 lines
1.1 KiB
Text
59 lines
1.1 KiB
Text
-- 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))
|