@@ -69,6 +69,10 @@ Examples:
6969def dropRight (s : String) (n : Nat) : String :=
7070 (s.dropEnd n).copy
7171
72+ @[deprecated Slice.dropEnd (since := "2025-11-20")]
73+ def Slice.dropRight (s : Slice) (n : Nat) : Slice :=
74+ s.dropEnd n
75+
7276@[export lean_string_dropright]
7377def Internal.dropRightImpl (s : String) (n : Nat) : String :=
7478 (String.dropEnd s n).copy
@@ -115,6 +119,10 @@ Examples:
115119def takeRight (s : String) (n : Nat) : String :=
116120 (s.takeEnd n).toString
117121
122+ @[deprecated Slice.takeEnd (since := "2025-11-20")]
123+ def Slice.takeRight (s : Slice) (n : Nat) : Slice :=
124+ s.takeEnd n
125+
118126/--
119127Creates a string slice that contains the longest prefix of {name}`s` in which {name}`pat` matched
120128(potentially repeatedly).
@@ -172,6 +180,10 @@ Examples:
172180def takeRightWhile (s : String) (p : Char → Bool) : String :=
173181 (s.takeEndWhile p).toString
174182
183+ @[deprecated Slice.takeEndWhile (since := "2025-11-20")]
184+ def Slice.takeRightWhile (s : Slice) (p : Char → Bool) : Slice :=
185+ s.takeEndWhile p
186+
175187/--
176188Creates a new string by removing the longest suffix from {name}`s` in which {name}`pat` matches
177189(potentially repeatedly).
@@ -193,6 +205,10 @@ Examples:
193205def dropRightWhile (s : String) (p : Char → Bool) : String :=
194206 (s.dropEndWhile p).toString
195207
208+ @[deprecated Slice.dropEndWhile (since := "2025-11-20")]
209+ def Slice.dropRightWhile (s : Slice) (p : Char → Bool) : Slice :=
210+ s.dropEndWhile p
211+
196212/--
197213Checks whether the first string ({name}`s`) begins with the pattern ({name}`pat`).
198214
@@ -263,6 +279,10 @@ Examples:
263279def trimRight (s : String) : String :=
264280 s.trimAsciiEnd.copy
265281
282+ @[deprecated Slice.trimAsciiEnd (since := "2025-11-20")]
283+ def Slice.trimRight (s : Slice) : Slice :=
284+ s.trimAsciiEnd
285+
266286/--
267287Removes leading whitespace from a string by returning a slice whose start position is the first
268288non-whitespace character, or the end position if there is no non-whitespace character.
@@ -283,6 +303,10 @@ Examples:
283303def trimLeft (s : String) : String :=
284304 s.trimAsciiStart.copy
285305
306+ @[deprecated Slice.trimAsciiStart (since := "2025-11-20")]
307+ def Slice.trimLeft (s : Slice) : Slice :=
308+ s.trimAsciiStart
309+
286310/--
287311Removes leading and trailing whitespace from a string.
288312
@@ -302,6 +326,10 @@ Examples:
302326def trim (s : String) : String :=
303327 s.trimAscii.copy
304328
329+ @[deprecated Slice.trimAscii (since := "2025-11-20")]
330+ def Slice.trim (s : Slice) : Slice :=
331+ s.trimAscii
332+
305333@[export lean_string_trim]
306334def Internal.trimImpl (s : String) : String :=
307335 (String.trimAscii s).copy
@@ -408,6 +436,10 @@ def dropPrefix [ForwardPattern ρ] (s : String) (pat : ρ) : String.Slice :=
408436def stripPrefix (s pre : String) : String :=
409437 (s.dropPrefix pre).toString
410438
439+ @[deprecated Slice.dropPrefix (since := "2025-11-20")]
440+ def Slice.stripPrefix (s pre : Slice) : Slice :=
441+ s.dropPrefix pre
442+
411443/--
412444If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`s` unmodified
413445otherwise.
@@ -432,4 +464,8 @@ def dropSuffix [BackwardPattern ρ] (s : String) (pat : ρ) : String.Slice :=
432464def stripSuffix (s : String) (suff : String) : String :=
433465 (s.dropSuffix suff).toString
434466
467+ @[deprecated Slice.dropSuffix (since := "2025-11-20")]
468+ def Slice.stripSuffix (s : Slice) (suff : Slice) : Slice :=
469+ s.dropSuffix suff
470+
435471end String
0 commit comments