From b856553b4fad16a6b674f5da1f70e646d647a7d6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 25 Oct 2020 21:55:50 +0100 Subject: [PATCH] chore: fix benchmark --- tests/bench/parser.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/tests/bench/parser.lean b/tests/bench/parser.lean index e3457f9726..3560876538 100644 --- a/tests/bench/parser.lean +++ b/tests/bench/parser.lean @@ -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"