From 6aa2ab65389a8a3ea71ae3a2f59035adaccb6375 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 21 Aug 2016 15:48:17 -0700
Subject: [PATCH] chore(tests/lean/run/match2): missing test

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

diff --git a/tests/lean/run/match2.lean b/tests/lean/run/match2.lean
new file mode 100644
index 0000000000..7d9d62d40d
--- /dev/null
+++ b/tests/lean/run/match2.lean
@@ -0,0 +1,7 @@
+inductive imf (f : nat → nat) : nat → Type
+| mk1 : ∀ (a : nat), imf (f a)
+| mk2 : imf (f 0 + 1)
+
+definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat \ x > b} →nat
+| .(f a)     (imf.mk1 .f a) x := a
+| .(f 0 + 1) (imf.mk2 .f)   x := subtype.elt_of x