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