Skip to content

Commit 3b152da

Browse files
committed
specialize -> inline
1 parent 6456655 commit 3b152da

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Init/Data/String/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2878,10 +2878,10 @@ Examples:
28782878
* `"coffee tea water".split (·.isWhitespace) = ["coffee", "", "tea", "", "water"]`
28792879
* `"fun x =>\n x + 1\n".split (· == '\n') = ["fun x =>", " x + 1", ""]`
28802880
-/
2881-
@[specialize] def splitToList (s : String) (p : Char → Bool) : List String :=
2881+
@[inline] def splitToList (s : String) (p : Char → Bool) : List String :=
28822882
splitAux s p 0 0 []
28832883

2884-
@[specialize, deprecated splitToList (since := "2025-10-17")]
2884+
@[inline, deprecated splitToList (since := "2025-10-17")]
28852885
def split (s : String) (p : Char → Bool) : List String :=
28862886
splitToList s p
28872887

0 commit comments

Comments
 (0)