lean4-htt/src/Init/Data/String
Markus Himmel eb01aaeee4
chore: rename String.Iterator to String.Legacy.Iterator (#11152)
This PR renames `String.Iterator` to `String.Legacy.Iterator`.

From the docstring of `String.Legacy.Iterator`:

> This is a no-longer-supported legacy API that will be removed in a
future release. You should use
> `String.ValidPos` instead, which is similar, but safer. To iterate
over a string `s`, start with
> `p : s.startValidPos`, advance it using `p.next`, access the current
character using `p.get` and
> check if the position is at the end using `p = s.endValidPos` or
`p.IsAtEnd`.
2025-11-13 13:46:22 +00:00
..
Lemmas feat: String.toList_map (#11021) 2025-11-01 13:54:39 +00:00
Pattern fix: KMP implementation (#10998) 2025-10-29 06:04:45 +00:00
Basic.lean perf: improve performance of String.ValidPos (#11142) 2025-11-11 15:30:47 +00:00
Bootstrap.lean refactor: use String.ofList and String.toList for String <-> List Char conversion (#11017) 2025-10-31 14:41:23 +00:00
Decode.lean perf: improve performance of String.ValidPos (#11142) 2025-11-11 15:30:47 +00:00
Defs.lean perf: improve performance of String.ValidPos (#11142) 2025-11-11 15:30:47 +00:00
Extra.lean refactor: do not use String.Iterator (#11127) 2025-11-11 11:46:58 +00:00
Iterator.lean chore: rename String.Iterator to String.Legacy.Iterator (#11152) 2025-11-13 13:46:22 +00:00
Lemmas.lean feat: String.toList_map (#11021) 2025-11-01 13:54:39 +00:00
Modify.lean feat: String.toList_map (#11021) 2025-11-01 13:54:39 +00:00
Pattern.lean feat: new String.Slice API (#10514) 2025-09-25 12:18:52 +00:00
PosRaw.lean chore: add deprecations for duplicated theorems (#10967) 2025-10-29 05:26:16 +00:00
Repr.lean refactor: do not use String.Iterator (#11127) 2025-11-11 11:46:58 +00:00
Search.lean refactor: do not use String.Iterator (#11127) 2025-11-11 11:46:58 +00:00
Slice.lean refactor: do not use String.Iterator (#11127) 2025-11-11 11:46:58 +00:00
Stream.lean refactor: move operations on String.Pos.Raw to the String.Pos.Raw namespace (#10735) 2025-10-18 12:12:55 +00:00
Substring.lean chore: move some material out of Init.Data.String.Basic (#10893) 2025-10-22 16:31:08 +00:00
TakeDrop.lean chore: move some material out of Init.Data.String.Basic (#10893) 2025-10-22 16:31:08 +00:00
Termination.lean feat: termination arguments for String.ValidPos and String.Slice.Pos (#10933) 2025-10-27 10:05:44 +00:00
ToSlice.lean refactor: redefine String.replace (#10986) 2025-10-29 07:48:33 +00:00