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

chore: fix benchmark

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-25 21:55:50 +01:00
parent b1b5460c4b
commit b856553b4f
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/bench/parser.lean
View file

@ -2,8 +2,7 @@ import Lean.Parser
def main : List String → IO Unit
| [fname, n] => do
env ← Lean.mkEmptyEnvironment;
n.toNat!.forM $ fun _ =>
discard $ Lean.Parser.parseFile env fname;
pure ()
let env ← Lean.mkEmptyEnvironment
for _ in [0:n.toNat!] do
discard $ Lean.Parser.parseFile env fname
| _ => throw $ IO.userError "give file"