From 6fe8a0e1793a2e75ca6c655fee8e6d090c2dc370 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Sep 2020 18:30:28 -0700
Subject: [PATCH] test: issue 29

New frontend fixed this issue.
closes #29
---
 tests/lean/run/29.lean | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 tests/lean/run/29.lean

diff --git a/tests/lean/run/29.lean b/tests/lean/run/29.lean
new file mode 100644
index 0000000000..605f2ce0c4
--- /dev/null
+++ b/tests/lean/run/29.lean
@@ -0,0 +1,6 @@
+new_frontend
+
+def foo : Nat -> Nat -> Nat -> List Nat
+| _, _, 0   => [1]
+| 0, _, _   => [2]
+| n, d, k+1 => foo n d k