From f2ee88aecf83a50cb32aaa375f4dac1327f76df8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Jun 2017 15:36:26 -0700
Subject: [PATCH] test(tests/lean/run/simp_rfl_proof_issue): add simp refl
 proof test

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

diff --git a/tests/lean/run/simp_rfl_proof_issue.lean b/tests/lean/run/simp_rfl_proof_issue.lean
new file mode 100644
index 0000000000..0b283611d1
--- /dev/null
+++ b/tests/lean/run/simp_rfl_proof_issue.lean
@@ -0,0 +1,16 @@
+@[irreducible] def f : nat → nat
+| 0     := 1
+| (n+1) := 2 * f n
+
+lemma ex1 (n : nat) : f (n+1) = 2 * f n :=
+begin
+  fail_if_success {refl},
+  simp only [f]
+end
+
+lemma ex2 (n : nat) (h : f (n+1) = 0) : 2 * f n = 0 :=
+begin
+  fail_if_success {exact h},
+  simp only [f] at h,
+  exact h
+end