From a171f8fbc353caf7341f2d7cf5dee473a19ac80b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Nov 2014 18:49:17 -0800
Subject: [PATCH] test(tests/lean/run): simple diag for square matrices

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

diff --git a/tests/lean/run/diag.lean b/tests/lean/run/diag.lean
new file mode 100644
index 000000000..af5f8856d
--- /dev/null
+++ b/tests/lean/run/diag.lean
@@ -0,0 +1,17 @@
+import data.vector
+open nat
+
+namespace vector
+
+definition diag {A} {n} : vector (vector A n) n → vector A n :=
+nat.rec_on n
+  (λv, nil)
+  (λn₁ (r : vector (vector A n₁) n₁ → vector A n₁) (v : vector (vector A (succ n₁)) (succ n₁)),
+    let h₁ : A                       := head (head v) in
+    let t₁ : vector (vector A n₁) n₁ := map tail (tail v) in
+    h₁ :: r t₁)
+
+example : diag ((1 :: 2 :: 3 :: nil) :: (4 :: 5 :: 6 :: nil) :: (7 :: 8 :: 9 :: nil) :: nil) = 1 :: 5 :: 9 :: nil :=
+rfl
+
+end vector