refactor: use String.ofList and String.toList for String <-> List Char conversion (#11017)

This PR establishes `String.ofList` and `String.toList` as the preferred
method for converting between strings and lists of characters and
deprecates the alternatives `String.mk`, `List.asString` and
`String.data`.

Author: TwoFX

src/Init/Data/BitVec/Basic.lean

@@ -203,8 +203,8 @@ If `n` is `0`, then one digit is returned. Otherwise, `⌊(n + 3) / 4⌋` digits
 -- `Internal` string functions by moving this definition out to a separate file that can live
 -- downstream of `Init.Data.String.Basic`.
 protected def toHex {n : Nat} (x : BitVec n) : String :=
-  let s := (Nat.toDigits 16 x.toNat).asString
-  let t := (List.replicate ((n+3) / 4 - String.Internal.length s) '0').asString
+  let s := String.ofList (Nat.toDigits 16 x.toNat)
+  let t := String.ofList (List.replicate ((n+3) / 4 - String.Internal.length s) '0')
   String.Internal.append t s
 
 /-- `BitVec` representation. -/

src/Init/Data/Repr.lean

@@ -226,7 +226,7 @@ Examples:
 -/
 @[extern "lean_string_of_usize"]
 protected def _root_.USize.repr (n : @& USize) : String :=
-  (toDigits 10 n.toNat).asString
+  String.ofList (toDigits 10 n.toNat)
 
 /-- We statically allocate and memoize reprs for small natural numbers. -/
 private def reprArray : Array String := Id.run do
@@ -235,14 +235,14 @@ private def reprArray : Array String := Id.run do
 def reprFast (n : Nat) : String :=
   if h : n < Nat.reprArray.size then Nat.reprArray.getInternal n h else
   if h : n < USize.size then (USize.ofNatLT n h).repr
-  else (toDigits 10 n).asString
+  else String.ofList (toDigits 10 n)
 
 /--
 Converts a natural number to its decimal string representation.
 -/
 @[implemented_by reprFast]
 protected def repr (n : Nat) : String :=
-  (toDigits 10 n).asString
+  String.ofList (toDigits 10 n)
 
 /--
 Converts a natural number less than `10` to the corresponding Unicode superscript digit character.
@@ -293,7 +293,7 @@ Examples:
  * `Nat.toSuperscriptString 35 = "³⁵"`
 -/
 def toSuperscriptString (n : Nat) : String :=
-  (toSuperDigits n).asString
+  String.ofList (toSuperDigits n)
 
 /--
 Converts a natural number less than `10` to the corresponding Unicode subscript digit character.
@@ -344,7 +344,7 @@ Examples:
  * `Nat.toSubscriptString 35 = "₃₅"`
 -/
 def toSubscriptString (n : Nat) : String :=
-  (toSubDigits n).asString
+  String.ofList (toSubDigits n)
 
 end Nat
 

src/Init/Data/String/Basic.lean

@@ -138,7 +138,7 @@ Examples:
 def String.ofList (data : List Char) : String :=
   ⟨List.utf8Encode data,.intro data rfl⟩
 
-@[extern "lean_string_mk", expose]
+@[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⟩
 
@@ -150,9 +150,9 @@ Examples:
  * `[].asString = ""`
  * `['a', 'a', 'a'].asString = "aaa"`
 -/
-@[expose, inline]
+@[expose, inline, deprecated String.ofList (since := "2025-10-30")]
 def List.asString (s : List Char) : String :=
-  String.mk s
+  String.ofList s
 
 namespace Substring.Internal
 

src/Init/Data/String/Bootstrap.lean

@@ -108,14 +108,23 @@ theorem String.bytes_inj {s t : String} : s.bytes = t.bytes ↔ s = t := by
   subst h
   rfl
 
-@[simp] theorem List.bytes_asString {l : List Char} : l.asString.bytes = l.utf8Encode := by
-  simp [List.asString, String.mk]
+@[simp] theorem String.bytes_ofList {l : List Char} : (String.ofList l).bytes = l.utf8Encode := by
+  simp [String.ofList]
 
-theorem String.exists_eq_asString (s : String) :
-    ∃ l : List Char, s = l.asString := by
+@[deprecated String.bytes_ofList (since := "2025-10-30")]
+theorem List.bytes_asString {l : List Char} : (String.ofList l).bytes = l.utf8Encode :=
+  String.bytes_ofList
+
+theorem String.exists_eq_ofList (s : String) :
+    ∃ l : List Char, s = String.ofList l := by
   rcases s with ⟨_, ⟨l, rfl⟩⟩
   refine ⟨l, by simp [← String.bytes_inj]⟩
 
+@[deprecated String.exists_eq_ofList (since := "2025-10-30")]
+theorem String.exists_eq_asString (s : String) :
+    ∃ l : List Char, s = String.ofList l :=
+  s.exists_eq_ofList
+
 @[simp]
 theorem String.utf8ByteSize_empty : "".utf8ByteSize = 0 := (rfl)
 
@@ -158,9 +167,13 @@ theorem utf8ByteSize_ofByteArray {b : ByteArray} {h} :
 theorem bytes_singleton {c : Char} : (String.singleton c).bytes = [c].utf8Encode := by
   simp [singleton]
 
-theorem singleton_eq_asString {c : Char} : String.singleton c = [c].asString := by
+theorem singleton_eq_ofList {c : Char} : String.singleton c = String.ofList [c] := by
   simp [← String.bytes_inj]
 
+@[deprecated singleton_eq_ofList (since := "2025-10-30")]
+theorem singleton_eq_asString {c : Char} : String.singleton c = String.ofList [c] :=
+  singleton_eq_ofList
+
 @[simp]
 theorem append_singleton {s : String} {c : Char} : s ++ singleton c = s.push c := by
   simp [← bytes_inj]
@@ -586,9 +599,6 @@ def Slice.Pos.byte {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : UInt8 :=
 
 @[simp] theorem default_eq : default = "" := rfl
 
-@[simp]
-theorem mk_eq_asString (s : List Char) : String.mk s = List.asString s := rfl
-
 theorem push_eq_append (c : Char) : String.push s c = s ++ singleton c := by
   simp
 

src/Init/Data/String/Defs.lean

@@ -19,10 +19,12 @@ open Std
 
 namespace String
 
-protected theorem data_eq_of_eq {a b : String} (h : a = b) : a.data = b.data :=
+@[deprecated toList_inj (since := "2025-10-30")]
+protected theorem data_eq_of_eq {a b : String} (h : a = b) : a.toList = b.toList :=
   h ▸ rfl
-protected theorem ne_of_data_ne {a b : String} (h : a.data ≠ b.data) : a ≠ b :=
-  fun h' => absurd (String.data_eq_of_eq h') h
+@[deprecated toList_inj (since := "2025-10-30")]
+protected theorem ne_of_data_ne {a b : String} (h : a.toList ≠ b.toList) : a ≠ b := by
+  simpa [← toList_inj]
 
 @[simp] protected theorem not_le {a b : String} : ¬ a ≤ b ↔ b < a := Decidable.not_not
 @[simp] protected theorem not_lt {a b : String} : ¬ a < b ↔ b ≤ a := Iff.rfl
@@ -34,7 +36,7 @@ attribute [local instance] Char.notLTTrans Char.notLTAntisymm Char.notLTTotal
 protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
 protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans
 protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total _ _
-protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.data) (bs := b.data) h₁ h₂)
+protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.toList) (bs := b.toList) h₁ h₂)
 protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
 protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
   have := String.lt_irrefl a

src/Init/Data/String/Lemmas.lean

@@ -160,11 +160,11 @@ Examples:
 -/
 @[extern "lean_string_utf8_set", expose]
 def Pos.Raw.set : String → (@& Pos.Raw) → Char → String
-  | s, i, c => (Pos.Raw.utf8SetAux c s.data 0 i).asString
+  | s, i, c => ofList (Pos.Raw.utf8SetAux c s.toList 0 i)
 
 @[extern "lean_string_utf8_set", expose, deprecated Pos.Raw.set (since := "2025-10-14")]
 def set : String → (@& Pos.Raw) → Char → String
-  | s, i, c => (Pos.Raw.utf8SetAux c s.data 0 i).asString
+  | s, i, c => ofList (Pos.Raw.utf8SetAux c s.toList 0 i)
 
 /--
 Replaces the character at position `p` in the string `s` with the result of applying `f` to that

src/Init/Data/String/Modify.lean

@@ -621,7 +621,7 @@ mutual
           asStringFn (atomicFn (noSpaceBefore >> repFn count (satisfyFn (· == char) s!"'{tok count}'"))))
 
   where
-    tok (count : Nat) : String := (List.replicate count char).asString
+    tok (count : Nat) : String := String.ofList (List.replicate count char)
     opener (ctxt : InlineCtxt) : ParserFn :=
       match getter ctxt with
       | none => many1Fn (satisfyFn (· == char) s!"any number of {char}s")
@@ -665,7 +665,7 @@ mutual
   where
     opener : ParserFn := asStringFn (many1Fn (satisfyFn (· == '`') s!"any number of backticks"))
     closer (count : Nat) : ParserFn :=
-      asStringFn (atomicFn (repFn count (satisfyFn' (· == '`') s!"expected '{String.mk (.replicate count '`')}' to close inline code"))) >>
+      asStringFn (atomicFn (repFn count (satisfyFn' (· == '`') s!"expected '{String.ofList (.replicate count '`')}' to close inline code"))) >>
       notFollowedByFn (satisfyFn (· == '`') "`") "backtick"
     takeBackticksFn : Nat → ParserFn
       | 0 => satisfyFn (fun _ => false)
@@ -1081,7 +1081,7 @@ mutual
               (closeFence l fenceWidth >>
                withFence 0 fun info _ c s =>
                 if (c.fileMap.toPosition info.getPos?.get!).column != col then
-                  s.mkErrorAt s!"closing '{String.mk <| List.replicate fenceWidth ':'}' from directive on line {l} at column {col}, but it's at column {(c.fileMap.toPosition info.getPos?.get!).column}" info.getPos?.get!
+                  s.mkErrorAt s!"closing '{String.ofList <| List.replicate fenceWidth ':'}' from directive on line {l} at column {col}, but it's at column {(c.fileMap.toPosition info.getPos?.get!).column}" info.getPos?.get!
                 else
                   s))
 
@@ -1114,7 +1114,7 @@ mutual
         else skipFn
 
     closeFence (line width : Nat) :=
-      let str := String.mk (.replicate width ':')
+      let str := String.ofList (.replicate width ':')
       bolThen (description := s!"closing '{str}' for directive from line {line}")
         (eatSpaces >>
          asStringFn (strFn str) >> notFollowedByFn (chFn ':') "':'" >>

src/Lean/DocString/Parser.lean

@@ -108,7 +108,7 @@ def mkMissingFieldsHint (fields : Array (Name × Option Expr)) (stx : Syntax) :
       match interveningLineEndPos? with
       | none => (.line, .nil)
       | some interveningLineEndPos =>
-        (String.mk (List.replicate (indent - col interveningLineEndPos) ' '), .nil)
+        (String.ofList (List.replicate (indent - col interveningLineEndPos) ' '), .nil)
   let suggestionText := preWs ++ suggestionText ++ postWs
   let insPos := view.lastFieldTailPos?.getD <| interveningLineEndPos?.getD view.leaderTailPos
   let width := Tactic.TryThis.format.inputWidth.get (← getOptions)

src/Lean/Elab/StructInstHint.lean

@@ -86,7 +86,7 @@ where
   stringContents : Parser String := attempt do
     let escaped := pchar '\\' *> pchar '"'
     let cs ← many (notFollowedBy (pchar '"') *> (escaped <|> any))
-    return String.mk cs.toList
+    return String.ofList cs.toList
 
   /--
   Parses all input up to the next whitespace. If `nonempty` is `true`, fails if there is no input