Skip to content

Commit b41ddea

Browse files
fgdoraisfgdorais
committed
chore: revert merging of #1736 
1 parent 36752f7 commit b41ddea

File tree

2 files changed

+25
-57
lines changed

2 files changed

+25
-57
lines changed

‎Batteries/Data/String/Legacy.lean‎

Lines changed: 25 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,6 @@ This file includes old definitions of `String` functions that were downstreamed
1414

1515
public section
1616

17-
set_option linter.deprecated false
18-
1917
namespace String
2018

2119
private noncomputable def utf8ByteSize' : String → Nat
@@ -71,8 +69,7 @@ private theorem mapAux_lemma (s : String) (i : Pos.Raw) (c : Char) (h : ¬i.atEn
7169
omega
7270

7371
/-- Implementation of `String.Legacy.map`. -/
74-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), specialize]
75-
def Legacy.mapAux (f : Char → Char) (i : Pos.Raw) (s : String) : String :=
72+
@[specialize] def Legacy.mapAux (f : Char → Char) (i : Pos.Raw) (s : String) : String :=
7673
if h : i.atEnd s then s
7774
else
7875
let c := f (i.get s)
@@ -92,8 +89,7 @@ Examples:
9289
* `"abc123".map Char.toUpper = "ABC123"`
9390
* `"".map Char.toUpper = ""`
9491
-/
95-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
96-
def Legacy.map (f : Char → Char) (s : String) : String :=
92+
@[inline] def Legacy.map (f : Char → Char) (s : String) : String :=
9793
mapAux f 0 s
9894

9995
/--
@@ -109,8 +105,7 @@ Examples:
109105
* `"red green blue".drop 10 = "blue"`
110106
* `"red green blue".drop 50 = ""`
111107
-/
112-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
113-
def Legacy.drop (s : String) (n : Nat) : String :=
108+
@[inline] def Legacy.drop (s : String) (n : Nat) : String :=
114109
(s.toRawSubstring.drop n).toString
115110

116111
/--
@@ -127,8 +122,7 @@ Examples:
127122
* `"red green blue".take 0 = ""`
128123
* `"red green blue".take 100 = "red green blue"`
129124
-/
130-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
131-
def Legacy.take (s : String) (n : Nat) : String :=
125+
@[inline] def Legacy.take (s : String) (n : Nat) : String :=
132126
(s.toRawSubstring.take n).toString
133127

134128
/--
@@ -144,8 +138,7 @@ Examples:
144138
* `"red green blue".takeWhile (· != 'n') = "red gree"`
145139
* `"red green blue".takeWhile (fun _ => true) = "red green blue"`
146140
-/
147-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
148-
def Legacy.takeWhile (s : String) (p : Char → Bool) : String :=
141+
@[inline] def Legacy.takeWhile (s : String) (p : Char → Bool) : String :=
149142
(s.toRawSubstring.takeWhile p).toString
150143

151144
/--
@@ -161,8 +154,7 @@ Examples:
161154
* `"red green blue".dropWhile (· != 'n') = "n blue"`
162155
* `"red green blue".dropWhile (fun _ => true) = ""`
163156
-/
164-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
165-
def Legacy.dropWhile (s : String) (p : Char → Bool) : String :=
157+
@[inline] def Legacy.dropWhile (s : String) (p : Char → Bool) : String :=
166158
(s.toRawSubstring.dropWhile p).toString
167159

168160
/--
@@ -171,8 +163,7 @@ Auxiliary definition for `String.Legacy.foldl`.
171163
This is an old implementation, preserved here for users of the lemmas in
172164
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.foldlAux`.
173165
-/
174-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), specialize]
175-
def Legacy.foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : Pos.Raw)
166+
@[specialize] def Legacy.foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : Pos.Raw)
176167
(i : Pos.Raw) (a : α) : α :=
177168
if h : i < stopPos then
178169
have := Nat.sub_lt_sub_left h (Pos.Raw.lt_next s i)
@@ -192,8 +183,7 @@ Examples:
192183
* `"coffee tea and water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3`
193184
* `"coffee tea water".foldl (·.push ·) "" = "coffee tea water"`
194185
-/
195-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
196-
def Legacy.foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α :=
186+
@[inline] def Legacy.foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α :=
197187
foldlAux f s s.rawEndPos 0 init
198188

199189
/--
@@ -206,8 +196,7 @@ Examples:
206196
* `"abc".front = 'a'`
207197
* `"".front = (default : Char)`
208198
-/
209-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline, expose]
210-
def Legacy.front (s : String) : Char :=
199+
@[inline, expose] def Legacy.front (s : String) : Char :=
211200
Pos.Raw.get s 0
212201

213202
/--
@@ -220,8 +209,7 @@ Examples:
220209
* `"abc".back = 'c'`
221210
* `"".back = (default : Char)`
222211
-/
223-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline, expose]
224-
def Legacy.back (s : String) : Char :=
212+
@[inline, expose] def Legacy.back (s : String) : Char :=
225213
(s.rawEndPos.prev s).get s
226214

227215
/--
@@ -230,7 +218,6 @@ Auxuliary definition for `String.Legacy.posOf`.
230218
This is an old implementation, preserved here for users of the lemmas in
231219
`Batteries.Data.String.Lemmas`.
232220
-/
233-
@[deprecated "Use the new `String` API." (since := "2026-03-26")]
234221
def Legacy.posOfAux (s : String) (c : Char) (stopPos : Pos.Raw) (pos : Pos.Raw) : Pos.Raw :=
235222
if h : pos < stopPos then
236223
if pos.get s == c then pos
@@ -252,8 +239,7 @@ Examples:
252239
* `"abcba".posOf 'z' = ⟨5⟩`
253240
* `"L∃∀N".posOf '∀' = ⟨4⟩`
254241
-/
255-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
256-
def Legacy.posOf (s : String) (c : Char) : Pos.Raw :=
242+
@[inline] def Legacy.posOf (s : String) (c : Char) : Pos.Raw :=
257243
posOfAux s c s.rawEndPos 0
258244

259245
/--
@@ -262,7 +248,6 @@ Auxuliary definition for `String.Legacy.revPosOf`.
262248
This is an old implementation, preserved here for users of the lemmas in
263249
`Batteries.Data.String.Lemmas`.
264250
-/
265-
@[deprecated "Use the new `String` API." (since := "2026-03-26")]
266251
def Legacy.revPosOfAux (s : String) (c : Char) (pos : Pos.Raw) : Option Pos.Raw :=
267252
if h : pos = 0 then none
268253
else
@@ -284,8 +269,7 @@ Examples:
284269
* `"abcabc".revPosOf 'z' = none`
285270
* `"L∃∀N".revPosOf '∀' = some ⟨4⟩`
286271
-/
287-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
288-
def Legacy.revPosOf (s : String) (c : Char) : Option Pos.Raw :=
272+
@[inline] def Legacy.revPosOf (s : String) (c : Char) : Option Pos.Raw :=
289273
revPosOfAux s c s.rawEndPos
290274

291275
/--
@@ -294,7 +278,6 @@ Auxuliary definition for `String.Legacy.find`.
294278
This is an old implementation, preserved here for users of the lemmas in
295279
`Batteries.Data.String.Lemmas`.
296280
-/
297-
@[deprecated "Use the new `String` API." (since := "2026-03-26")]
298281
def Legacy.findAux (s : String) (p : Char → Bool) (stopPos : Pos.Raw) (pos : Pos.Raw) : Pos.Raw :=
299282
if h : pos < stopPos then
300283
if p (pos.get s) then pos
@@ -317,8 +300,7 @@ Examples:
317300
* `"tea".find (· == 'X') = ⟨3⟩`
318301
* `"".find (· == 'X') = ⟨0⟩`
319302
-/
320-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
321-
def Legacy.find (s : String) (p : Char → Bool) : Pos.Raw :=
303+
@[inline] def Legacy.find (s : String) (p : Char → Bool) : Pos.Raw :=
322304
findAux s p s.rawEndPos 0
323305

324306
/--
@@ -327,7 +309,6 @@ Auxuliary definition for `String.Legacy.revFind`.
327309
This is an old implementation, preserved here for users of the lemmas in
328310
`Batteries.Data.String.Lemmas`.
329311
-/
330-
@[deprecated "Use the new `String` API." (since := "2026-03-26")]
331312
def Legacy.revFindAux (s : String) (p : Char → Bool) (pos : Pos.Raw) : Option Pos.Raw :=
332313
if h : pos = 0 then none
333314
else
@@ -349,8 +330,7 @@ Examples:
349330
* `"tea".revFind (· == 'X') = none`
350331
* `"".revFind (· == 'X') = none`
351332
-/
352-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
353-
def Legacy.revFind (s : String) (p : Char → Bool) : Option Pos.Raw :=
333+
@[inline] def Legacy.revFind (s : String) (p : Char → Bool) : Option Pos.Raw :=
354334
revFindAux s p s.rawEndPos
355335

356336
/--
@@ -359,8 +339,7 @@ Auxuliary definition for `String.Legacy.foldr`.
359339
This is an old implementation, preserved here for users of the lemmas in
360340
`Batteries.Data.String.Lemmas`.
361341
-/
362-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), specialize]
363-
def Legacy.foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String)
342+
@[specialize] def Legacy.foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String)
364343
(i begPos : Pos.Raw) : α :=
365344
if h : begPos < i then
366345
have := Pos.Raw.prev_lt_of_pos s i <| mt (congrArg String.Pos.Raw.byteIdx) <|
@@ -383,8 +362,7 @@ Examples:
383362
* `"coffee tea and water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3`
384363
* `"coffee tea water".foldr (fun c s => c.push s) "" = "retaw dna aet eeffoc"`
385364
-/
386-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
387-
def Legacy.foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α :=
365+
@[inline] def Legacy.foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α :=
388366
foldrAux f init s s.rawEndPos 0
389367

390368
/--
@@ -393,8 +371,7 @@ Auxuliary definition for `String.Legacy.any`.
393371
This is an old implementation, preserved here for users of the lemmas in
394372
`Batteries.Data.String.Lemmas`.
395373
-/
396-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), specialize]
397-
def Legacy.anyAux (s : String) (stopPos : Pos.Raw) (p : Char → Bool) (i : Pos.Raw) :
374+
@[specialize] def Legacy.anyAux (s : String) (stopPos : Pos.Raw) (p : Char → Bool) (i : Pos.Raw) :
398375
Bool :=
399376
if h : i < stopPos then
400377
if p (i.get s) then true
@@ -418,8 +395,7 @@ Examples:
418395
* `"brown and orange".any (·.isLetter) = true`
419396
* `"".any (fun _ => false) = false`
420397
-/
421-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
422-
def Legacy.any (s : String) (p : Char → Bool) : Bool :=
398+
@[inline] def Legacy.any (s : String) (p : Char → Bool) : Bool :=
423399
anyAux s s.rawEndPos p 0
424400

425401
/--
@@ -435,8 +411,7 @@ Examples:
435411
* `"brown and orange".all (·.isLetter) = false`
436412
* `"".all (fun _ => false) = true`
437413
-/
438-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
439-
def Legacy.all (s : String) (p : Char → Bool) : Bool :=
414+
@[inline] def Legacy.all (s : String) (p : Char → Bool) : Bool :=
440415
!Legacy.any s (fun c => !p c)
441416

442417
/--
@@ -450,8 +425,7 @@ Examples:
450425
* `"green".contains 'x' = false`
451426
* `"".contains 'x' = false`
452427
-/
453-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
454-
def Legacy.contains (s : String) (c : Char) : Bool :=
428+
@[inline] def Legacy.contains (s : String) (c : Char) : Bool :=
455429
Legacy.any s (fun a => a == c)
456430

457431
end String
@@ -465,8 +439,7 @@ accumulated value is combined with each character in order, using `f`.
465439
This is an old implementation, preserved here for users of the lemmas in
466440
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `Substring.Raw.foldl`.
467441
-/
468-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
469-
def Legacy.foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring.Raw) : α :=
442+
@[inline] def Legacy.foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring.Raw) : α :=
470443
match s with
471444
| ⟨s, b, e⟩ => String.Legacy.foldlAux f s e b init
472445

@@ -477,8 +450,7 @@ accumulated value is combined with each character in reverse order, using `f`.
477450
This is an old implementation, preserved here for users of the lemmas in
478451
`Batteries.Data.String.Lemmas`.
479452
-/
480-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
481-
def Legacy.foldr {α : Type u} (f : Char → α → α) (init : α) (s : Substring.Raw) : α :=
453+
@[inline] def Legacy.foldr {α : Type u} (f : Char → α → α) (init : α) (s : Substring.Raw) : α :=
482454
match s with
483455
| ⟨s, b, e⟩ => String.Legacy.foldrAux f init s e b
484456

@@ -490,8 +462,7 @@ Short-circuits at the first character for which `p` returns `true`.
490462
This is an old implementation, preserved here for users of the lemmas in
491463
`Batteries.Data.String.Lemmas`.
492464
-/
493-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
494-
def Legacy.any (s : Substring.Raw) (p : Char → Bool) : Bool :=
465+
@[inline] def Legacy.any (s : Substring.Raw) (p : Char → Bool) : Bool :=
495466
match s with
496467
| ⟨s, b, e⟩ => String.Legacy.anyAux s e p b
497468

@@ -503,8 +474,7 @@ Short-circuits at the first character for which `p` returns `false`.
503474
This is an old implementation, preserved here for users of the lemmas in
504475
`Batteries.Data.String.Lemmas`.
505476
-/
506-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
507-
def Legacy.all (s : Substring.Raw) (p : Char → Bool) : Bool :=
477+
@[inline] def Legacy.all (s : Substring.Raw) (p : Char → Bool) : Bool :=
508478
!Legacy.any s (fun c => !p c)
509479

510480
/--
@@ -513,8 +483,7 @@ Checks whether a substring contains the specified character.
513483
This is an old implementation, preserved here for users of the lemmas in
514484
`Batteries.Data.String.Lemmas`.
515485
-/
516-
@[deprecated "Use the new `String` API." (since := "2026-03-26"), inline]
517-
def Legacy.contains (s : Substring.Raw) (c : Char) : Bool :=
486+
@[inline] def Legacy.contains (s : Substring.Raw) (c : Char) : Bool :=
518487
Legacy.any s (fun a => a == c)
519488

520489
end Substring.Raw

‎Batteries/Data/String/Lemmas.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ import all Init.Data.String.Modify -- for unfolding `String.mapAux`
2020
import all Batteries.Data.String.Legacy -- for unfolding `String.Legacy.map`
2121
import all Init.Data.String.Legacy -- for unfolding `String.splitOnAux`
2222

23-
set_option linter.deprecated false in
2423
@[expose] public section
2524

2625
namespace String

0 commit comments

Comments
 (0)