refactor: move String.ofList to the Prelude (#12029)

This PR moves `String.ofList` to `Init.Prelude`. It is a function that
the Lean kernel expects to be present and has special support for (when
reducing string literals). By moving this to `Init.Prelude`, all
declarations that are special to the kernel are in that single module.

(cherry picked from commit 9167b13
and aac353c)

Author: nomeata

src/Init/Data/String/Bootstrap.lean

@@ -123,18 +123,6 @@ opaque getUTF8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8
 
 end String.Internal
 
-/--
-Creates a string that contains the characters in a list, in order.
-
-Examples:
- * `['L', '∃', '∀', 'N'].asString = "L∃∀N"`
- * `[].asString = ""`
- * `['a', 'a', 'a'].asString = "aaa"`
--/
-@[extern "lean_string_mk", expose]
-def String.ofList (data : List Char) : String :=
-  ⟨List.utf8Encode data,.intro data rfl⟩
-
 @[extern "lean_string_mk", expose, deprecated String.ofList (since := "2025-10-30")]
 def String.mk (data : List Char) : String :=
   ⟨List.utf8Encode data,.intro data rfl⟩

src/Init/Prelude.lean

@@ -3470,6 +3470,18 @@ structure String where ofByteArray ::
 attribute [extern "lean_string_to_utf8"] String.toByteArray
 attribute [extern "lean_string_from_utf8_unchecked"] String.ofByteArray
 
+/--
+Creates a string that contains the characters in a list, in order.
+
+Examples:
+ * `String.ofList ['L', '∃', '∀', 'N'] = "L∃∀N"`
+ * `String.ofList [] = ""`
+ * `String.ofList ['a', 'a', 'a'] = "aaa"`
+-/
+@[extern "lean_string_mk"]
+def String.ofList (data : List Char) : String :=
+  ⟨List.utf8Encode data, .intro data rfl⟩
+
 /--
 Decides whether two strings are equal. Normally used via the `DecidableEq String` instance and the
 `=` operator.