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 2024-06-20 18:18:41 +02:00 • committed by GitHub
parent 1f732bb3b7
commit d6eab393f4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/bench/workspaceSymbols.lean
View file

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