From 2c12bc9fdf4ab5483080b8f2bd2a663f76e3a51e Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 20 Nov 2025 14:09:52 +0100
Subject: [PATCH] chore: more deprecations for string migration (#11281)

This PR adds a few deprecations for functions that never existed but
that are still helpful for people migrating their code post-#11180.
---
 src/Init/Data/String/TakeDrop.lean | 36 ++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/src/Init/Data/String/TakeDrop.lean b/src/Init/Data/String/TakeDrop.lean
index 18dffe1844..f00c258f21 100644
--- a/src/Init/Data/String/TakeDrop.lean
+++ b/src/Init/Data/String/TakeDrop.lean
@@ -69,6 +69,10 @@ Examples:
 def dropRight (s : String) (n : Nat) : String :=
   (s.dropEnd n).copy
 
+@[deprecated Slice.dropEnd (since := "2025-11-20")]
+def Slice.dropRight (s : Slice) (n : Nat) : Slice :=
+  s.dropEnd n
+
 @[export lean_string_dropright]
 def Internal.dropRightImpl (s : String) (n : Nat) : String :=
   (String.dropEnd s n).copy
@@ -115,6 +119,10 @@ Examples:
 def takeRight (s : String) (n : Nat) : String :=
   (s.takeEnd n).toString
 
+@[deprecated Slice.takeEnd (since := "2025-11-20")]
+def Slice.takeRight (s : Slice) (n : Nat) : Slice :=
+  s.takeEnd n
+
 /--
 Creates a string slice that contains the longest prefix of {name}`s` in which {name}`pat` matched
 (potentially repeatedly).
@@ -172,6 +180,10 @@ Examples:
 def takeRightWhile (s : String) (p : Char → Bool) : String :=
   (s.takeEndWhile p).toString
 
+@[deprecated Slice.takeEndWhile (since := "2025-11-20")]
+def Slice.takeRightWhile (s : Slice) (p : Char → Bool) : Slice :=
+  s.takeEndWhile p
+
 /--
 Creates a new string by removing the longest suffix from {name}`s` in which {name}`pat` matches
 (potentially repeatedly).
@@ -193,6 +205,10 @@ Examples:
 def dropRightWhile (s : String) (p : Char → Bool) : String :=
   (s.dropEndWhile p).toString
 
+@[deprecated Slice.dropEndWhile (since := "2025-11-20")]
+def Slice.dropRightWhile (s : Slice) (p : Char → Bool) : Slice :=
+  s.dropEndWhile p
+
 /--
 Checks whether the first string ({name}`s`) begins with the pattern ({name}`pat`).
 
@@ -263,6 +279,10 @@ Examples:
 def trimRight (s : String) : String :=
   s.trimAsciiEnd.copy
 
+@[deprecated Slice.trimAsciiEnd (since := "2025-11-20")]
+def Slice.trimRight (s : Slice) : Slice :=
+  s.trimAsciiEnd
+
 /--
 Removes leading whitespace from a string by returning a slice whose start position is the first
 non-whitespace character, or the end position if there is no non-whitespace character.
@@ -283,6 +303,10 @@ Examples:
 def trimLeft (s : String) : String :=
   s.trimAsciiStart.copy
 
+@[deprecated Slice.trimAsciiStart (since := "2025-11-20")]
+def Slice.trimLeft (s : Slice) : Slice :=
+  s.trimAsciiStart
+
 /--
 Removes leading and trailing whitespace from a string.
 
@@ -302,6 +326,10 @@ Examples:
 def trim (s : String) : String :=
   s.trimAscii.copy
 
+@[deprecated Slice.trimAscii (since := "2025-11-20")]
+def Slice.trim (s : Slice) : Slice :=
+  s.trimAscii
+
 @[export lean_string_trim]
 def Internal.trimImpl (s : String) : String :=
   (String.trimAscii s).copy
@@ -408,6 +436,10 @@ def dropPrefix [ForwardPattern ρ] (s : String) (pat : ρ) : String.Slice :=
 def stripPrefix (s pre : String) : String :=
   (s.dropPrefix pre).toString
 
+@[deprecated Slice.dropPrefix (since := "2025-11-20")]
+def Slice.stripPrefix (s pre : Slice) : Slice :=
+  s.dropPrefix pre
+
 /--
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`s` unmodified
 otherwise.
@@ -432,4 +464,8 @@ def dropSuffix [BackwardPattern ρ] (s : String) (pat : ρ) : String.Slice :=
 def stripSuffix (s : String) (suff : String) : String :=
   (s.dropSuffix suff).toString
 
+@[deprecated Slice.dropSuffix (since := "2025-11-20")]
+def Slice.stripSuffix (s : Slice) (suff : Slice) : Slice :=
+  s.dropSuffix suff
+
 end String