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

perf: use mkArray in fuzzyMatchCore

Browse source
This commit is contained in:
Sebastian Ullrich 2022-03-03 11:54:11 +01:00 • committed by Leonardo de Moura
parent d48c5b99e9
commit ff11325fce
1 changed files with 1 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Data/FuzzyMatching.lean
View file

@ -94,10 +94,7 @@ bonus.
`patternComplete` is necessary to know when we are behind the match in the
word. -/
private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Array CharRole) (patternComplete := true) : Option Int := Id.run <| do
let mut result : Array (Option Int) := Array.mkEmpty ((pattern.length + 1) * (word.length + 1) * 2)
for _ in [:(pattern.length + 1) * (word.length + 1) * 2] do
result := result.push none
let mut result : Array (Option Int) := Array.mkArray ((pattern.length + 1) * (word.length + 1) * 2) none
result := set result 0 0 (some 0) none