From 70f7ec3cf27176170a67c7b8732404447888c8c4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 20 Dec 2014 11:36:32 -0800
Subject: [PATCH] test(tests/lean/hott): add test for 'cases' tactic

---
 tests/lean/hott/cases.hlean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 tests/lean/hott/cases.hlean

diff --git a/tests/lean/hott/cases.hlean b/tests/lean/hott/cases.hlean
new file mode 100644
index 000000000..bfad630b2
--- /dev/null
+++ b/tests/lean/hott/cases.hlean
@@ -0,0 +1,19 @@
+open nat
+
+inductive vec (A : Type) : nat → Type :=
+nil {} : vec A zero,
+cons   : Π {n}, A → vec A n → vec A (succ n)
+
+namespace vec
+  variables {A B C : Type}
+  variables {n m : nat}
+  notation a :: b := cons a b
+
+  protected definition destruct (v : vec A (succ n)) {P : Π {n : nat}, vec A (succ n) → Type}
+                      (H : Π {n : nat} (h : A) (t : vec A n), P (h :: t)) : P v :=
+  begin
+    cases v with (n', h', t'),
+    apply (H h' t')
+  end
+
+end vec