docs: add docstrings and usage examples in Init.Data.String.Basic

Add docstrings  and usage examples for `String.length`, `.push`,
`.append`, `.get?`, `.set`, `.modyify`, and `.next`. Update docstrings
and add usage examples for `String.toList`, `.get`, and `.get!`.

src/Init/Data/String/Basic.lean

@@ -24,23 +24,41 @@ instance : LT String :=
 instance decLt (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
   List.hasDecidableLt s₁.data s₂.data
 
+/--
+Returns the length of a string.
+* `"".length = 0`
+* `"abc".length = 3`
+-/
 @[extern "lean_string_length"]
 def length : (@& String) → Nat
   | ⟨s⟩ => s.length
 
-/-- The internal implementation uses dynamic arrays and will perform destructive updates
-   if the String is not shared. -/
+/--
+Pushes a character onto the end of a string.
+
+The internal implementation uses dynamic arrays and will perform destructive updates
+if the String is not shared.
+* `"abc".push 'd' = "abcd"`
+-/
 @[extern "lean_string_push"]
 def push : String → Char → String
   | ⟨s⟩, c => ⟨s ++ [c]⟩
 
-/-- The internal implementation uses dynamic arrays and will perform destructive updates
-   if the String is not shared. -/
+/--
+Appends two strings.
+
+The internal implementation uses dynamic arrays and will perform destructive updates
+if the String is not shared.
+* `"abc".append "def" = "abcdef"`
+-/
 @[extern "lean_string_append"]
 def append : String → (@& String) → String
   | ⟨a⟩, ⟨b⟩ => ⟨a ++ b⟩
 
-/-- O(n) in the runtime, where n is the length of the String -/
+/--
+`O(s.length)`. Converts a string to a list of characters.
+* `"abc".toList = ['a', 'b', 'c']`
+-/
 def toList (s : String) : List Char :=
   s.data
 
@@ -59,9 +77,13 @@ def utf8GetAux : List Char → Pos → Pos → Char
   | c::cs, i, p => if i = p then c else utf8GetAux cs (i + c) p
 
 /--
-  Return character at position `p`. If `p` is not a valid position
-  returns `(default : Char)`.
-  See `utf8GetAux` for the reference implementation.
+Returns the character at position `p` of a string.
+
+If `p` is not a valid position, returns `(default : Char)`.
+
+See `utf8GetAux` for the reference implementation.
+* `"abc".get ⟨1⟩ = 'b'`
+* `"abc".get ⟨3⟩ = (default : Char) = 'A'`
 -/
 @[extern "lean_string_utf8_get"]
 def get (s : @& String) (p : @& Pos) : Char :=
@@ -72,12 +94,21 @@ def utf8GetAux? : List Char → Pos → Pos → Option Char
   | [],    _, _ => none
   | c::cs, i, p => if i = p then c else utf8GetAux? cs (i + c) p
 
+/--
+Returns the character at position `p`.
+
+If `p` is not a valid position, returns `none`.
+* `"abc".get ⟨1⟩ = some 'b'`
+* `"abc".get ⟨3⟩ = none`
+-/
 @[extern "lean_string_utf8_get_opt"]
 def get? : (@& String) → (@& Pos) → Option Char
   | ⟨s⟩, p => utf8GetAux? s 0 p
 
 /--
-  Similar to `get`, but produces a panic error message if `p` is not a valid `String.Pos`.
+Similar to `get`, but produces a panic error message if `p` is not a valid `String.Pos`.
+* `"abc".get! ⟨1⟩ = 'b'`
+* `"abc".get! ⟨3⟩ => panic!`
 -/
 @[extern "lean_string_utf8_get_bang"]
 def get! (s : @& String) (p : @& Pos) : Char :=
@@ -89,13 +120,34 @@ def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
   | c::cs, i, p =>
     if i = p then (c'::cs) else c::(utf8SetAux c' cs (i + c) p)
 
+/--
+Replaces the character at a specified position in a string with a new character.
+
+If the position is invalid, returns the string unchanged.
+* `"abc".set ⟨1⟩ 'B' = "aBc"`
+* `"abc".set ⟨3⟩ 'D' = "abc"`
+-/
 @[extern "lean_string_utf8_set"]
 def set : String → (@& Pos) → Char → String
   | ⟨s⟩, i, c => ⟨utf8SetAux c s 0 i⟩
 
+/--
+Applies `f` to the character at position `p` in the string `s`.
+
+If `p` is an invalid position, returns the string unchanged.
+* `abc.modify ⟨1⟩ Char.toUpper = "aBc"`
+* `abc.modify ⟨3⟩ Char.toUpper = "abc"`
+-/
 def modify (s : String) (i : Pos) (f : Char → Char) : String :=
   s.set i <| f <| s.get i
 
+/--
+Returns the next position in a string after `p`.
+
+Note `p.next` is not necessarily a valid position in the string `s`.
+* `"abc".next ⟨1⟩ = String.Pos.mk 2`
+* `"abc".next ⟨3⟩ = String.Pos.mk 4`
+-/
 @[extern "lean_string_utf8_next"]
 def next (s : @& String) (p : @& Pos) : Pos :=
   let c := get s p