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

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

diff --git a/tests/lean/run/eq8.lean b/tests/lean/run/eq8.lean
new file mode 100644
index 000000000..6e76166ed
--- /dev/null
+++ b/tests/lean/run/eq8.lean
@@ -0,0 +1,6 @@
+import data.vector
+open vector
+
+definition map {A B C : Type} (f : A → B → C) : Π {n}, vector A n → vector B n → vector C n,
+map nil nil             := nil,
+map (a :: va) (b :: vb) := f a b :: map va vb