From 7106d3fb34a9774b267b69be33ece111cfa41c21 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 3 Mar 2022 11:23:47 +0100 Subject: [PATCH] perf: specialize `iterateLookaround` --- src/Lean/Data/FuzzyMatching.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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