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