diff --git a/tests/lean/run/1797.lean b/tests/lean/run/1797.lean
new file mode 100644
index 0000000000..cdd45d979d
--- /dev/null
+++ b/tests/lean/run/1797.lean
@@ -0,0 +1,6 @@
+example (n : nat) : true :=
+begin
+  cases h : n with m,
+  { guard_hyp h := n = nat.zero, admit },
+  { guard_hyp h := n = nat.succ m, admit}
+end