test: issue 29

New frontend fixed this issue.
closes #29
This commit is contained in:
Leonardo de Moura 2020-09-23 18:30:28 -07:00
parent e22d2f6cb1
commit 6fe8a0e179

6
tests/lean/run/29.lean Normal file
View file

@ -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