From 204d950a5f6087f4980614ce3cb013ff7dfa50af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Aug 2016 14:45:21 -0700
Subject: [PATCH] test(tests/lean/run/def13): add map-like test for dependent
 patter matching

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

diff --git a/tests/lean/run/def13.lean b/tests/lean/run/def13.lean
new file mode 100644
index 0000000000..5e5d423ed4
--- /dev/null
+++ b/tests/lean/run/def13.lean
@@ -0,0 +1,20 @@
+set_option new_elaborator true
+
+inductive vec (A : Type) : nat → Type
+| nil {} : vec 0
+| cons   : Π {n}, A → vec n → vec (n+1)
+
+open vec
+
+variables {A : Type}
+variables f : A → A → A
+
+definition map_head_1 : ∀ {n}, vec A n → vec A n → vec A n
+| .0     nil nil                       := nil
+| .(n+1) (@cons .A n a va) (cons b vb) := cons (f a b) va
+
+example : map_head_1 f nil nil = nil :=
+rfl
+
+example (a b : A) (n : nat) (va vb : vec A n) : map_head_1 f (cons a va) (cons b vb) = cons (f a b) va :=
+rfl