From ff11325fce9732ce07449cbc35e27c602cfa3efd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 3 Mar 2022 11:54:11 +0100 Subject: [PATCH] perf: use `mkArray` in `fuzzyMatchCore` --- src/Lean/Data/FuzzyMatching.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Lean/Data/FuzzyMatching.lean b/src/Lean/Data/FuzzyMatching.lean index 69e3f6d770..fb08e62129 100644 --- a/src/Lean/Data/FuzzyMatching.lean +++ b/src/Lean/Data/FuzzyMatching.lean @@ -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