From bd9f54cfe78323e1078c77ec4515f3fa30e44add Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 2 Jul 2017 10:15:00 -0700
Subject: [PATCH] test(tests/lean/run/1675): `simp_all` and `let`

---
 tests/lean/run/1675.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/tests/lean/run/1675.lean b/tests/lean/run/1675.lean
index 440dfaddc4..06b4657d7f 100644
--- a/tests/lean/run/1675.lean
+++ b/tests/lean/run/1675.lean
@@ -38,3 +38,11 @@ begin
   simp_all {fail_if_unchanged := ff}, -- should work
   admit
 end
+
+example (p : Prop) : let h : 0 = 0 := rfl in p :=
+begin
+  intro h,
+  simp_all,
+  do {e₁ ← get_local `h >>= infer_type, e₂ ← to_expr ```(true), guard (e₁ = e₂)},
+  admit
+end