nat.dk

(; Natural numbers and elementary operations ;)

Nat : Type.
succ : Nat -> Nat.
0 : Nat.

def 1 := succ 0.
def 2 := succ 1.
def 3 := succ 2.
def 4 := succ 3.
def 5 := succ 4.
def 6 := succ 5.
def 7 := succ 6.
def 8 := succ 7.
def 9 := succ 8.

(; Addition ;)
def add : Nat -> Nat -> Nat.
[X] add 0 X --> X
[X, Y] add (succ X) Y --> succ (add X Y).

(; Multiplication ;)
def mul : Nat -> Nat -> Nat.
[X] mul 0 X --> 0
[X, Y] mul (succ X) Y --> add Y (mul X Y).

(; Exponentiation: exp x y = y^x ;)
def exp : Nat -> Nat -> Nat.
[X] exp 0 X --> 1
[X, Y] exp (succ X) Y --> mul Y (exp X Y).

(; Factorial ;)
def fac : Nat -> Nat.
[] fac 0 --> 1
[] fac (succ 0) --> 1
[X] fac (succ X) --> mul (succ X) (fac X).

(; Fibonacci ;)
def fib : Nat -> Nat.
[] fib 0 --> 0
[] fib (succ 0) --> 1
[X] fib (succ (succ X)) --> add (fib (succ X)) (fib X).

(; A dependent type used to check equality ;)
Dep : Nat -> Type.
dep : n : Nat -> Dep n.