From 3af8ca11bc49d24961e7ae4629fffa60213eda26 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 Sep 2017 14:36:51 -0700
Subject: [PATCH] chore(tests/lean/run/1797): add test for #1797

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

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