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

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

diff --git a/tests/lean/run/eq7.lean b/tests/lean/run/eq7.lean
new file mode 100644
index 0000000000..a98f799917
--- /dev/null
+++ b/tests/lean/run/eq7.lean
@@ -0,0 +1,13 @@
+import data.vector
+open nat vector
+
+definition diag {A : Type} : Π {n}, vector (vector A n) n → vector A n,
+diag nil               := nil,
+diag ((a :: va) :: vs) := a :: diag (map tail vs)
+
+theorem diag_nil (A : Type) : diag (@nil (vector A 0)) = nil :=
+rfl
+
+theorem diag_succ {A : Type} {n : nat} (a : A) (va : vector A n) (vs : vector (vector A (succ n)) n) :
+    diag ((a :: va) :: vs) = a :: diag (map tail vs) :=
+rfl