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

chore(tests/compiler/t2): fix test

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-15 14:42:59 +01:00 • committed by Leonardo de Moura
parent b8900fad80
commit 03456ab752
2 changed files with 1 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/compiler/t2.lean
View file

@ -78,7 +78,7 @@ instance : has_to_string Expr :=
def nest_aux (s : nat) (f : nat → Expr → io Expr) : nat → Expr → io Expr
| 0 x := pure x
| m@(n+1) x := (timeit "step: " $ f (s - m) x) >>= nest_aux n
| m@(n+1) x := f (s - m) x >>= nest_aux n
def nest (f : nat → Expr → io Expr) (n : nat) (e : Expr) : io Expr :=
nest_aux n f n e

9
tests/compiler/t2.lean.expected.out
View file

@ -1,18 +1,9 @@
1 count: 6
step: 0.0313ms
2 count: 22
step: 0.0137ms
3 count: 90
step: 0.0109ms
4 count: 420
step: 0.0442ms
5 count: 2202
step: 0.177ms
6 count: 12886
step: 0.945ms
7 count: 83648
step: 5.1ms
8 count: 598592
step: 38ms
9 count: 4697200
step: 289ms