From 7488378445eeea73caa275e95676d4aad62a6213 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 4 Jan 2015 17:50:41 -0800
Subject: [PATCH] test(tests/lean/run): define list append using recursive
 equations

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

diff --git a/tests/lean/run/eq6.lean b/tests/lean/run/eq6.lean
new file mode 100644
index 000000000..1a8784f4d
--- /dev/null
+++ b/tests/lean/run/eq6.lean
@@ -0,0 +1,15 @@
+import data.list
+open list
+
+definition append {A : Type} : list A → list A → list A,
+append nil      l := l,
+append (h :: t) l := h :: (append t l)
+
+theorem append_nil {A : Type} (l : list A) : append nil l = l :=
+rfl
+
+theorem append_cons {A : Type} (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) :=
+rfl
+
+example : append (1 :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) :=
+rfl