refactor: use String.ofList and String.toList for String <-> List Char conversion

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/Bootstrap.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/Defs.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/Lemmas.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/Modify.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/Lean/DocString/Parser.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/Elab/StructInstHint.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/ErrorExplanation.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

src/Lean/Meta/Hint.lean

@@ -196,8 +196,8 @@ such as `b̵a̵c̲h̲e̲e̲rs̲`.
 -/
 private def mkDiffString (ds : Array (Diff.Action × String)) : String :=
   let rangeStrs := ds.map fun
-    | (.insert, s) => String.mk (s.data.flatMap ([·, '\u0332'])) -- U+0332 Combining Low Line
-    | (.delete, s) => String.mk (s.data.flatMap ([·, '\u0335'])) -- U+0335 Combining Short Stroke Overlay
+    | (.insert, s) => String.ofList (s.toList.flatMap ([·, '\u0332'])) -- U+0332 Combining Low Line
+    | (.delete, s) => String.ofList (s.toList.flatMap ([·, '\u0335'])) -- U+0335 Combining Short Stroke Overlay
     | (.skip  , s) => s
   rangeStrs.foldl (· ++ ·) ""
 
@@ -277,7 +277,7 @@ partial def readableDiff (s s' : String) (granularity : DiffGranularity := .auto
     -- front and back, or at a single interior point. This will always be fairly readable (and
     -- splitting by a larger unit would likely only be worse)
     if charArrDiff.size ≤ 3 || approxEditDistance ≤ maxCharDiffDistance then
-      charArrDiff.map fun (act, cs) => (act, String.mk cs.toList)
+      charArrDiff.map fun (act, cs) => (act, String.ofList cs.toList)
     else if approxEditDistance ≤ maxWordDiffDistance then
       wordDiff
     else
@@ -375,14 +375,14 @@ where
 
   /-- Given a `Char` diff, produces an equivalent `String` diff, joining actions of the same kind. -/
   joinCharDiff (d : Array (Diff.Action × Char)) :=
-    joinEdits d |>.map fun (act, cs) => (act, String.mk cs.toList)
+    joinEdits d |>.map fun (act, cs) => (act, String.ofList cs.toList)
 
   maxDiff :=
     #[(.delete, s), (.insert, s')]
 
   mkWhitespaceDiff (oldWs newWs : String) :=
     if !oldWs.contains '\n' then
-      Diff.diff oldWs.data.toArray newWs.data.toArray |> joinCharDiff
+      Diff.diff oldWs.toList.toArray newWs.toList.toArray |> joinCharDiff
     else
       #[(.skip, newWs)]
 

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -1894,7 +1894,7 @@ def anchorPrefixToString (numDigits : Nat) (anchorPrefix : UInt64) : String :=
   let n := cs.length
   let zs := List.replicate (numDigits - n) '0'
   let cs := zs ++ cs
-  cs.asString
+  String.ofList cs
 
 def anchorToString (numDigits : Nat) (anchor : UInt64) : String :=
   anchorPrefixToString numDigits (anchor >>> (64 - 4*numDigits.toUInt64))

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -31,8 +31,8 @@ private partial def reduceListChar (e : Expr) (s : String) : SimpM DStep := do
   else
     return .continue
 
-builtin_dsimproc [simp, seval] reduceMk (String.mk _) := fun e => do
-  unless e.isAppOfArity ``String.mk 1 do return .continue
+builtin_dsimproc [simp, seval] reduceOfList (String.ofList _) := fun e => do
+  unless e.isAppOfArity ``String.ofList 1 do return .continue
   reduceListChar e.appArg! ""
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : String → String → Bool) (e : Expr) : SimpM Step := do

src/lake/Lake/Build/Trace.lean

@@ -139,7 +139,7 @@ public def ofHex? (s : String) : Option Hash :=
 
 /-- Returns the hash as 16-digit lowercase hex string. -/
 public def hex (self : Hash) : String :=
-  lpad (Nat.toDigits 16 self.val.toNat).asString '0' 16
+  lpad (String.ofList <| Nat.toDigits 16 self.val.toNat) '0' 16
 
 public def ofDecimal? (s : String) : Option Hash :=
   (inline s.toNat?).map ofNat

src/lake/Lake/Toml/Data/Value.lean

@@ -65,7 +65,7 @@ public def ppString (s : String) : String :=
     | '\\' => s ++ "\\\\"
     | _ =>
       if c.val < 0x20 || c.val == 0x7F then
-        s ++ "\\u" ++ lpad (String.mk <| Nat.toDigits 16 c.val.toNat) '0' 4
+        s ++ "\\u" ++ lpad (String.ofList <| Nat.toDigits 16 c.val.toNat) '0' 4
       else
         s.push c
   s.push '\"'