Docs and tests

Author: TwoFX

src/Init/Data/String/Search.lean

@@ -6,16 +6,15 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.String.Defs
-public import Init.Data.Iterators.Combinators.FilterMap
-public import Init.Data.String.Pattern
-public import Init.Data.String.ToSlice
 public import Init.Data.String.Slice
 
 set_option doc.verso true
 
 /-!
-# String API
+# String operations based on slice operations
+
+This file contains {name}`String` operations that are implemented by passing to
+{name}`String.Slice`.
 -/
 
 public section
@@ -35,10 +34,16 @@ variable [∀ s, Std.Iterators.IteratorLoop (σ s) Id Id]
 Constructs a new string obtained by replacing all occurrences of {name}`pattern` with
 {name}`replacement` in {name}`s`.
 
+This function is generic over all currently supported patterns. The replacement may be a
+{name}`String` or a {name}`String.Slice`.
+
 Examples:
+* {lean}`"red green blue".replace 'e' "" = "rd grn blu"`
+* {lean}`"red green blue".replace (fun c => c == 'u' || c == 'e') "" = "rd grn bl"`
 * {lean}`"red green blue".replace "e" "" = "rd grn blu"`
 * {lean}`"red green blue".replace "ee" "E" = "red grEn blue"`
 * {lean}`"red green blue".replace "e" "E" = "rEd grEEn bluE"`
+* {lean}`"aaaaa".replace "aa" "b" = "bba"`
 * {lean}`"abc".replace "" "k" = "kakbkck"`
 -/
 @[inline]

src/Init/Data/String/Slice.lean

@@ -360,10 +360,16 @@ def dropPrefix [ForwardPattern ρ] (s : Slice) (pat : ρ) : Slice :=
 Constructs a new string obtained by replacing all occurrences of {name}`pattern` with
 {name}`replacement` in {name}`s`.
 
+This function is generic over all currently supported patterns. The replacement may be a
+{name}`String` or a {name}`String.Slice`.
+
 Examples:
+* {lean}`"red green blue".toSlice.replace 'e' "" = "rd grn blu"`
+* {lean}`"red green blue".toSlice.replace (fun c => c == 'u' || c == 'e') "" = "rd grn bl"`
 * {lean}`"red green blue".toSlice.replace "e" "" = "rd grn blu"`
 * {lean}`"red green blue".toSlice.replace "ee" "E" = "red grEn blue"`
 * {lean}`"red green blue".toSlice.replace "e" "E" = "rEd grEEn bluE"`
+* {lean}`"aaaaa".toSlice.replace "aa" "b" = "bba"`
 * {lean}`"abc".toSlice.replace "" "k" = "kakbkck"`
 -/
 def replace [ToForwardSearcher ρ σ] [ToSlice α] (s : Slice) (pattern : ρ) (replacement : α) :

tests/lean/run/string_replace.lean

@@ -0,0 +1,17 @@
+def isVowel (c : Char) : Bool :=
+  c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u'
+
+#guard "education".replace isVowel "☃!" = "☃!d☃!c☃!t☃!☃!n"
+#guard "red green blue".replace "e" "" = "rd grn blu"
+#guard "red green blue".replace 'e' "" = "rd grn blu"
+#guard "red green blue".replace "ee" "E" = "red grEn blue"
+#guard "red green blue".replace "e" "E" = "rEd grEEn bluE"
+#guard "abc".replace "" "k" = "kakbkck"
+#guard "ℕ".replace "" "z" = "zℕz"
+#guard "𝔸".replace "" "z" = "z𝔸z"
+#guard "v̂".replace "" "z" = "zvẑz"
+#guard "aaaaa".replace "aa" "b" = "bba"
+#guard "v̂fℚo".replace ("ℕfℚoℤ".toSlice.drop 1 |>.dropEnd 1) ("☃🔭🌌".toSlice.dropEnd 1 |>.drop 1) = "v̂🔭"
+#guard ("abcde".toSlice.drop 1).replace (· == 'c') "C" = "bCde"
+#guard (("ac  bc  cc  cd".toSlice.split "  ").map (·.replace 'c' "C") |>.toList) = ["aC", "bC", "CC", "Cd"]
+#guard "red green blue".replace (fun c => c == 'u' || c == 'e') "" = "rd grn bl"