chore: missing docstring + style updates for String docs (#10640)

This PR adds a missing docstring and applies our style guide to parts of
the String API.

Author: david-christiansen

src/Init/Data/String/Basic.lean

@@ -1010,10 +1010,9 @@ theorem ValidPos.isValidUTF8_extract {s : String} (pos₁ pos₂ : s.ValidPos) :
 /--
 A region or slice of some underlying string.
 
-A substring contains an string together with the start and end byte positions of a region of
+A slice consists of a string together with the start and end byte positions of a region of
 interest. Actually extracting a substring requires copying and memory allocation, while many
-substrings of the same underlying string may exist with very little overhead, and they are more
-convenient than tracking the bounds by hand.
+slices of the same underlying string may exist with very little overhead. While this could be achieved by tracking the bounds by hand, the slice API is much more convenient.
 
 `String.Slice` bundles proofs to ensure that the start and end positions always delineate a valid
 string. For this reason, it should be preferred over `Substring`.
@@ -1031,6 +1030,9 @@ structure Slice where
 instance : Inhabited Slice where
   default := ⟨"", "".startValidPos, "".startValidPos, by simp [Pos.Raw.le_iff]⟩
 
+/--
+Returns a slice that contains the entire string.
+-/
 @[inline, expose] -- expose for the defeq `s.toSlice.str = s`.
 def toSlice (s : String) : Slice where
   str := s

src/Init/Data/String/Pattern/Basic.lean

@@ -14,12 +14,12 @@ set_option doc.verso true
 /-!
 This module defines the notion of patterns which is central to the {name}`String.Slice` and
 {name}`String` API. All functions on {name}`String.Slice` and {name}`String` that
-"search for something" are polymorphic over a pattern instead of taking just one particular kind
+“search for something” are polymorphic over a pattern instead of taking just one particular kind
 of pattern such as a {name}`Char`. The key components are:
 - {name (scope := "Init.Data.String.Pattern.Basic")}`ToForwardSearcher`
 - {name (scope := "Init.Data.String.Pattern.Basic")}`ForwardPattern`
 - {name (scope := "Init.Data.String.Pattern.Basic")}`ToBackwardSearcher`
-- {name (scope := "Init.Data.String.Pattern.Basic")}`SuffixPattern`
+- {name (scope := "Init.Data.String.Pattern.Basic")}`BackwardPattern`
 -/
 
 public section
@@ -41,12 +41,12 @@ inductive SearchStep (s : Slice) where
 deriving Inhabited
 
 /--
-Provides a conversion from a pattern to an iterator of {name}`SearchStep` searching for matches of
-the pattern from the start towards the end of a {name}`Slice`.
+Provides a conversion from a pattern to an iterator of {name}`SearchStep` that searches for matches
+of the pattern from the start towards the end of a {name}`Slice`.
 -/
 class ToForwardSearcher (ρ : Type) (σ : outParam (Slice → Type)) where
   /--
-  Build an iterator of {name}`SearchStep` corresponding to matches of {name}`pat` along the slice
+  Builds an iterator of {name}`SearchStep` corresponding to matches of {name}`pat` along the slice
   {name}`s`. The {name}`SearchStep`s returned by this iterator must contain ranges that are
   adjacent, non-overlapping and cover all of {name}`s`.
   -/
@@ -56,8 +56,8 @@ class ToForwardSearcher (ρ : Type) (σ : outParam (Slice → Type)) where
 Provides simple pattern matching capabilities from the start of a {name}`Slice`.
 
 While these operations can be implemented on top of {name}`ToForwardSearcher` some patterns allow
-for more efficient implementations so this class can be used to specialise for them. If there is no
-need to specialise in this fashion
+for more efficient implementations. This class can be used to specialize for them. If there is no
+need to specialize in this fashion, then
 {name (scope := "Init.Data.String.Pattern.Basic")}`ForwardPattern.defaultImplementation` can be used
 to automatically derive an instance.
 -/
@@ -67,8 +67,8 @@ class ForwardPattern (ρ : Type) where
   -/
   startsWith : Slice → ρ → Bool
   /--
-  Checks whether the slice starts with the pattern, if it does return slice with the prefix removed,
-  otherwise {name}`none`.
+  Checks whether the slice starts with the pattern. If it does, the slice is returned with the
+  prefix removed; otherwise the result is {name}`none`.
   -/
   dropPrefix? : Slice → ρ → Option Slice
 
@@ -181,14 +181,21 @@ class ToBackwardSearcher (ρ : Type) (σ : outParam (Slice → Type)) where
 /--
 Provides simple pattern matching capabilities from the end of a {name}`Slice`.
 
-While these operations can be implemented on top of {name}`ToBackwardSearcher` some patterns allow
-for more efficient implementations so this class can be used to specialise for them. If there is no
-need to specialise in this fashion
+While these operations can be implemented on top of {name}`ToBackwardSearcher`, some patterns allow
+for more efficient implementations. This class can be used to specialize for them. If there is no
+need to specialize in this fashion, then
 {name (scope := "Init.Data.String.Pattern.Basic")}`BackwardPattern.defaultImplementation` can be
 used to automatically derive an instance.
 -/
 class BackwardPattern (ρ : Type) where
+  /--
+  Checks whether the slice ends with the pattern.
+  -/
   endsWith : Slice → ρ → Bool
+  /--
+  Checks whether the slice ends with the pattern. If it does, the slice is returned with the
+  suffix removed; otherwise the result is {name}`none`.
+  -/
   dropSuffix? : Slice → ρ → Option Slice
 
 namespace ToBackwardSearcher

src/Init/Data/String/Slice.lean

@@ -707,7 +707,7 @@ deriving Inhabited
 
 set_option doc.verso false
 /--
-Creates and iterator over all valid positions within {name}`s`.
+Creates an iterator over all valid positions within {name}`s`.
 
 Examples
  * {lean}`("abc".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', 'c']`
@@ -776,7 +776,7 @@ docs_to_verso positions
 end PosIterator
 
 /--
-Creates and iterator over all characters (Unicode code points) in {name}`s`.
+Creates an iterator over all characters (Unicode code points) in {name}`s`.
 
 Examples:
  * {lean}`"abc".toSlice.chars.toList = ['a', 'b', 'c']`
@@ -792,7 +792,7 @@ deriving Inhabited
 
 set_option doc.verso false
 /--
-Creates and iterator over all valid positions within {name}`s`, starting from the last valid
+Creates an iterator over all valid positions within {name}`s`, starting from the last valid
 position and iterating towards the first one.
 
 Examples
@@ -863,7 +863,7 @@ docs_to_verso revPositions
 end RevPosIterator
 
 /--
-Creates and iterator over all characters (Unicode code points) in {name}`s`, starting from the end
+Creates an iterator over all characters (Unicode code points) in {name}`s`, starting from the end
 of the slice and iterating towards the start.
 
 Example:
@@ -881,7 +881,7 @@ deriving Inhabited
 
 set_option doc.verso false
 /--
-Creates and iterator over all bytes in {name}`s`.
+Creates an iterator over all bytes in {name}`s`.
 
 Examples:
  * {lean}`"abc".toSlice.bytes.toList = [97, 98, 99]`
@@ -955,7 +955,7 @@ structure RevByteIterator where
 
 set_option doc.verso false
 /--
-Creates and iterator over all bytes in {name}`s`, starting from the last one and iterating towards
+Creates an iterator over all bytes in {name}`s`, starting from the last one and iterating towards
 the first one.
 
 Examples: