From 1c1cfdd0105fdb564790b5c0407afac3056f5ed2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Dec 2015 23:32:13 -0800
Subject: [PATCH] test(tests/lean/run): add Dan's reducible+ematch test

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

diff --git a/tests/lean/run/blast_ematch9.lean b/tests/lean/run/blast_ematch9.lean
new file mode 100644
index 000000000..450e2671b
--- /dev/null
+++ b/tests/lean/run/blast_ematch9.lean
@@ -0,0 +1,8 @@
+constant P : nat → Prop
+definition h [reducible] (n : nat) := n
+definition foo [forward] : ∀ x, P (h x) := sorry
+
+set_option blast.ematch true
+
+example (n : nat) : P (h n) :=
+by blast