chore: deprecate String.toSubstring (#11232)

This PR deprecates `String.toSubstring` in favor of
`String.toRawSubstring` (cf. #11154).

Author: TwoFX

src/Init/Data/String/Defs.lean

@@ -631,4 +631,12 @@ def Slice.Pos.byte {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : UInt8 :=
 theorem push_eq_append (c : Char) : String.push s c = s ++ singleton c := by
   simp
 
+@[deprecated String.toRawSubstring (since := "2025-11-18")]
+def toSubstring (s : String) : Substring.Raw :=
+  s.toRawSubstring
+
+@[deprecated String.toRawSubstring' (since := "2025-11-18")]
+def toSubstring' (s : String) : Substring.Raw :=
+  s.toRawSubstring'
+
 end String

src/Init/Prelude.lean

@@ -3517,14 +3517,6 @@ Converts a `String` into a `Substring` that denotes the entire string.
   startPos := {}
   stopPos  := s.rawEndPos
 
-/--
-Converts a `String` into a `Substring` that denotes the entire string.
--/
-@[inline] def String.toSubstring (s : String) : Substring.Raw where
-  str      := s
-  startPos := {}
-  stopPos  := s.rawEndPos
-
 /--
 Converts a `String` into a `Substring` that denotes the entire string.
 
@@ -3533,14 +3525,6 @@ This is a version of `String.toRawSubstring` that doesn't have an `@[inline]` an
 def String.toRawSubstring' (s : String) : Substring.Raw :=
   s.toRawSubstring
 
-/--
-Converts a `String` into a `Substring` that denotes the entire string.
-
-This is a version of `String.toRawSubstring` that doesn't have an `@[inline]` annotation.
--/
-def String.toSubstring' (s : String) : Substring.Raw :=
-  s.toRawSubstring
-
 /--
 This function will cast a value of type `α` to type `β`, and is a no-op in the
 compiler. This function is **extremely dangerous** because there is no guarantee