diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
index c22ab020bd..26fc953dc6 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
@@ -52,6 +52,12 @@ builtin_dsimproc [simp, seval] reduceSingleton (String.singleton _) := fun e =>
   let some c ← Char.fromExpr? e.appArg! | return .continue
   return .done <| toExpr (String.singleton c)
 
+builtin_dsimproc_decl reduceToSingleton ((_ : String)) := fun e => do
+  let some s ← fromExpr? e | return .continue
+  let l := s.toList
+  let [c] := l | return .continue
+  return .done <| mkApp (mkConst ``String.singleton) (toExpr c)
+
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : String → String → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
diff --git a/tests/elab/simprocString.lean b/tests/elab/simprocString.lean
index 842ad19c02..e046473f7d 100644
--- a/tests/elab/simprocString.lean
+++ b/tests/elab/simprocString.lean
@@ -55,5 +55,14 @@ example : String.singleton ' ' = " " := by simp
 example : String.singleton 'a' = "a" := by simp
 example : String.singleton '\n' = "\n" := by simp
 
+-- String.reduceToSingleton (not in default simp set)
+example : "a" = String.singleton 'a' := by simp only [String.reduceToSingleton]
+example : " " = String.singleton ' ' := by simp only [String.reduceToSingleton]
+example : "\n" = String.singleton '\n' := by simp only [String.reduceToSingleton]
+-- Multi-character strings should not be reduced
+example : "ab" = "ab" := by simp only [String.reduceToSingleton]
+-- Empty strings should not be reduced
+example : "" = "" := by simp only [String.reduceToSingleton]
+
 -- Combined: roundtrip toList/ofList
 example : String.ofList "hello".toList = "hello" := by simp