From e301f86c6cbded82d59294751c72114c183aed89 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 18 Nov 2025 11:41:22 +0100 Subject: [PATCH] chore: add `String.Pos.next` (#11238) This PR is split from a future PR and adds the function `String.Pos.next`, an alias (and soon to be correct name) of `String.ValidPos.next`. This is for boring bootstrapping reasons. --- src/Init/Data/String/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 6461c4485e..1f4754dcae 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1599,6 +1599,10 @@ position is not the past-the-end position, which guarantees that such a position def ValidPos.next {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos := ((inline (Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)))).ofSlice) +@[expose, extern "lean_string_utf8_next_fast"] +def Pos.next {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos := + ((inline (Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)))).ofSlice) + /-- Advances a valid position on a string to the next valid position, or returns `none` if the given position is the past-the-end position. -/ @[inline, expose]