Skip to content

Commit 6562487

Browse files
committed
Fix typo
1 parent e384902 commit 6562487

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

src/Init/Data/String/Search.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ Examples:
3939
* {lean}`"red green blue".replace "e" "" = "rd grn blu"`
4040
* {lean}`"red green blue".replace "ee" "E" = "red grEn blue"`
4141
* {lean}`"red green blue".replace "e" "E" = "rEd grEEn bluE"`
42-
* {lean}`"abc".replace "" "k" = "rakbkck"`
42+
* {lean}`"abc".replace "" "k" = "kakbkck"`
4343
-/
4444
@[inline]
4545
def replace [ToForwardSearcher ρ σ] [ToSlice α] (s : String) (pattern : ρ)

src/Init/Data/String/Slice.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -364,7 +364,7 @@ Examples:
364364
* {lean}`"red green blue".toSlice.replace "e" "" = "rd grn blu"`
365365
* {lean}`"red green blue".toSlice.replace "ee" "E" = "red grEn blue"`
366366
* {lean}`"red green blue".toSlice.replace "e" "E" = "rEd grEEn bluE"`
367-
* {lean}`"abc".toSlice.replace "" "k" = "rakbkck"`
367+
* {lean}`"abc".toSlice.replace "" "k" = "kakbkck"`
368368
-/
369369
def replace [ToForwardSearcher ρ σ] [ToSlice α] (s : Slice) (pattern : ρ) (replacement : α) :
370370
String :=

0 commit comments

Comments
 (0)