From 1a8840330f6534ecb9e4ebe02703360dba0b36cf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Mar 2022 12:57:46 -0700 Subject: [PATCH] test: add test for example that does not work in Lean3 cc @eric-wieser --- tests/lean/run/wfLean3Issue.lean | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 tests/lean/run/wfLean3Issue.lean diff --git a/tests/lean/run/wfLean3Issue.lean b/tests/lean/run/wfLean3Issue.lean new file mode 100644 index 0000000000..f65609d9b7 --- /dev/null +++ b/tests/lean/run/wfLean3Issue.lean @@ -0,0 +1,6 @@ +def foo : Nat → Nat → Nat + | 0, 0 => 1 + | s+1, 0 => foo s 0 + 1 + | 0, b+1 => foo 0 b + 1 + | s+1, b+1 => foo (s+1) b + foo s (b+1) +termination_by foo b s => (b, s)