From d6eab393f4df9d473b5736d636b178eb26d197e6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 20 Jun 2024 18:18:41 +0200 Subject: [PATCH] chore: fix benchmark --- tests/bench/workspaceSymbols.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/bench/workspaceSymbols.lean b/tests/bench/workspaceSymbols.lean index 92cc74c2c8..8612cce112 100644 --- a/tests/bench/workspaceSymbols.lean +++ b/tests/bench/workspaceSymbols.lean @@ -4,7 +4,7 @@ open Lean Elab def bench (pattern : String) : TermElabM Unit := do let env ← getEnv let mut n := 0 - IO.println s!"{env.constants.size} decls" + -- IO.println s!"{env.constants.size} decls" for (c, _) in env.constants.toList do if Lean.FuzzyMatching.fuzzyMatch pattern c.toString then n := n + 1 IO.println s!"{n} matches"