21 lines
344 B
Plaintext
21 lines
344 B
Plaintext
--#print Nat
|
|
#eval Lean.versionString
|
|
|
|
def fib (n:Nat):Nat :=
|
|
match n with
|
|
| 0 => 1
|
|
| 1 => 1
|
|
| n+2 => fib (n+1) + fib n
|
|
|
|
example : fib 5 = 8 := rfl
|
|
|
|
example : fib (n+2) = fib (n+1) + fib n := rfl
|
|
|
|
def ack : Nat -> Nat -> Nat
|
|
| 0, y => y+1
|
|
| x+1, 0 => ack x 1
|
|
| x+1, y+1 => ack x (ack (x+1) y)
|
|
termination_by ack x y => (x, y)
|
|
|
|
|