michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lean/run): define ackermann function using recursors

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-11 11:06:10 -08:00
parent 21b93bd2e5
commit b3e4a689cf
1 changed files with 27 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
tests/lean/run/ack.lean Normal file
View file

@ -0,0 +1,27 @@
import data.nat.basic
open nat
definition iter (f : nat → nat) (n : nat) : nat :=
nat.rec_on n
(f 1)
(λ (n₁ : nat) (r : nat), f r)
definition ack (m : nat) : nat → nat :=
nat.rec_on m
nat.succ
(λ (m₁ : nat) (r : nat → nat), iter r)
theorem ack_0_n (n : nat) : ack 0 n = n + 1 :=
rfl
theorem ack_m_0 (m : nat) : ack (m + 1) 0 = ack m 1 :=
rfl
theorem ack_m_n (m n : nat) : ack (m + 1) (n + 1) = ack m (ack (m + 1) n) :=
rfl
example : ack 3 2 = 29 :=
rfl
example : ack 3 3 = 61 :=
rfl