max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/lean/run): add test for performance issue reported in the lean group

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-12 10:38:23 -08:00
parent 6e3959de2f
commit 7794ecfb69
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/run/even.lean Normal file
View file

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