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

perf: specialize iterateLookaround

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

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

@ -42,7 +42,7 @@ def charRole (prev? : Option CharType) (curr : CharType) (next?: Option CharType
CharRole.head
private def iterateLookaround (f : (Option Char × Char × Option Char) → α) (string : String) : Array α :=
@[specialize] private def iterateLookaround (f : (Option Char × Char × Option Char) → α) (string : String) : Array α :=
if string.isEmpty then
#[]
else if string.length == 1 then