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

doc: fix wrong example for String.split (#13787)

Browse source 
This PR fixes a small docsting error for `String.split`.
This commit is contained in:
Christian Krause 2026-05-21 12:17:58 +02:00 • committed by GitHub
parent 8f49fe9864
commit df2a367958
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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/Init/Data/String/Search.lean
View file

@ -251,7 +251,7 @@ Examples:
* {lean}`("coffee tea water".split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
* {lean}`("coffee tea water".split " tea ").toList == ["coffee".toSlice, "water".toSlice]`
* {lean}`("ababababa".split "aba").toList == ["coffee".toSlice, "water".toSlice]`
* {lean}`("ababababa".split "aba").toList == ["".toSlice, "b".toSlice, "ba".toSlice]`
* {lean}`("baaab".split "aa").toList == ["b".toSlice, "ab".toSlice]`
-/
@[inline]