From 7794ecfb695cd8206bdb446ae67e311eeed9d4f9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Dec 2016 10:38:23 -0800 Subject: [PATCH] test(tests/lean/run): add test for performance issue reported in the lean group --- tests/lean/run/even.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/lean/run/even.lean diff --git a/tests/lean/run/even.lean b/tests/lean/run/even.lean new file mode 100644 index 0000000000..5914dea3f3 --- /dev/null +++ b/tests/lean/run/even.lean @@ -0,0 +1,12 @@ +open nat + +def even : nat → bool +| 0 := tt +| (succ 0) := ff +| (succ (succ n)) := even n + +vm_eval even 0 +vm_eval even 1 +vm_eval even 2 +vm_eval even 10000 +vm_eval even 10001