diff --git a/src/Lean/Data/FuzzyMatching.lean b/src/Lean/Data/FuzzyMatching.lean index 6f3dfcf916..b772aeb7c6 100644 --- a/src/Lean/Data/FuzzyMatching.lean +++ b/src/Lean/Data/FuzzyMatching.lean @@ -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