From 7fca862fc3957e4fede404c7fe2c9b90950248d9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 4 Jan 2015 17:47:18 -0800
Subject: [PATCH] test(tests/lean/run): define fibonacci using recursive
 equations

---
 tests/lean/run/eq5.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 tests/lean/run/eq5.lean

diff --git a/tests/lean/run/eq5.lean b/tests/lean/run/eq5.lean
new file mode 100644
index 000000000..62186f0cf
--- /dev/null
+++ b/tests/lean/run/eq5.lean
@@ -0,0 +1,18 @@
+open nat
+
+definition fib : nat → nat,
+fib 0     := 1,
+fib 1     := 1,
+fib (x+2) := fib x + fib (x+1)
+
+theorem fib0 : fib 0 = 1 :=
+rfl
+
+theorem fib1 : fib 1 = 1 :=
+rfl
+
+theorem fib_succ_succ (a : nat) : fib (a+2) = fib a + fib (a+1) :=
+rfl
+
+example : fib 8 = 34 :=
+rfl