Remove inline annotation

.github/workflows/pr-release.yml

@@ -43,19 +43,6 @@ jobs:
           name: build-.*
           name_is_regexp: true
 
-      # Verify artifacts were downloaded before any side effects (tag creation, release deletion).
-      - name: Verify release artifacts exist
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          shopt -s nullglob
-          files=(artifacts/*/*)
-          if [ ${#files[@]} -eq 0 ]; then
-            echo "::error::No artifacts found matching artifacts/*/*"
-            exit 1
-          fi
-          echo "Found ${#files[@]} artifacts to upload:"
-          printf '%s\n' "${files[@]}"
-
       - name: Push tag
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
@@ -87,6 +74,18 @@ jobs:
           gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} -y || true
         env:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+      # Verify artifacts were downloaded (equivalent to fail_on_unmatched_files in the old action).
+      - name: Verify release artifacts exist
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        run: |
+          shopt -s nullglob
+          files=(artifacts/*/*)
+          if [ ${#files[@]} -eq 0 ]; then
+            echo "::error::No artifacts found matching artifacts/*/*"
+            exit 1
+          fi
+          echo "Found ${#files[@]} artifacts to upload:"
+          printf '%s\n' "${files[@]}"
       # We use `gh release create` instead of `softprops/action-gh-release` because
       # the latter enumerates all releases to check for existing ones, which fails
       # when the repository has more than 10000 releases (GitHub API pagination limit).

src/Init/Data/String.lean

@@ -26,3 +26,4 @@ public import Init.Data.String.ToSlice
 public import Init.Data.String.Search
 public import Init.Data.String.Legacy
 public import Init.Data.String.Grind
+public import Init.Data.String.Subslice

src/Init/Data/String/Basic.lean

@@ -1722,6 +1722,16 @@ theorem Slice.Pos.offset_cast {s t : Slice} {pos : s.Pos} {h : s = t} :
 theorem Slice.Pos.cast_rfl {s : Slice} {pos : s.Pos} : pos.cast rfl = pos :=
   Slice.Pos.ext (by simp)
 
+@[simp]
+theorem Slice.Pos.cast_le_cast_iff {s t : Slice} {pos pos' : s.Pos} {h : s = t} :
+    pos.cast h ≤ pos'.cast h ↔ pos ≤ pos' := by
+  cases h; simp
+
+@[simp]
+theorem Slice.Pos.cast_lt_cast_iff {s t : Slice} {pos pos' : s.Pos} {h : s = t} :
+    pos.cast h < pos'.cast h ↔ pos < pos' := by
+  cases h; simp
+
 /-- Constructs a valid position on `t` from a valid position on `s` and a proof that `s = t`. -/
 @[inline]
 def Pos.cast {s t : String} (pos : s.Pos) (h : s = t) : t.Pos where
@@ -1956,6 +1966,7 @@ theorem Pos.ne_startPos_of_lt {s : String} {p q : s.Pos} :
     Pos.Raw.byteIdx_zero]
   omega
 
+@[simp]
 theorem Pos.next_ne_startPos {s : String} {p : s.Pos} {h} :
     p.next h ≠ s.startPos :=
   ne_startPos_of_lt p.lt_next
@@ -1992,6 +2003,7 @@ theorem Pos.ne_of_lt {s : String} {p q : s.Pos} : p < q → p ≠ q := by
 theorem Pos.lt_of_lt_of_le {s : String} {p q r : s.Pos} : p < q → q ≤ r → p < r := by
   simpa [Pos.lt_iff, Pos.le_iff] using Pos.Raw.lt_of_lt_of_le
 
+@[simp]
 theorem Pos.le_endPos {s : String} (p : s.Pos) : p ≤ s.endPos := by
   simpa [Pos.le_iff] using p.isValid.le_rawEndPos
 

src/Init/Data/String/Defs.lean

@@ -399,7 +399,7 @@ achieved by tracking the bounds by hand, the slice API is much more convenient.
 string. For this reason, it should be preferred over `Substring.Raw`.
 -/
 structure Slice where
-  /-- The underlying strings. -/
+  /-- The underlying string. -/
   str : String
   /-- The byte position of the start of the string slice. -/
   startInclusive : str.Pos
@@ -441,6 +441,18 @@ def Slice.utf8ByteSize (s : Slice) : Nat :=
 theorem Slice.utf8ByteSize_eq {s : Slice} :
     s.utf8ByteSize = s.endExclusive.offset.byteIdx - s.startInclusive.offset.byteIdx := (rfl)
 
+/--
+Checks whether a slice is empty.
+
+Empty slices have {name}`utf8ByteSize` {lean}`0`.
+
+Examples:
+ * {lean}`"".toSlice.isEmpty = true`
+ * {lean}`" ".toSlice.isEmpty = false`
+-/
+@[inline]
+def Slice.isEmpty (s : Slice) : Bool := s.utf8ByteSize == 0
+
 instance : HAdd Pos.Raw Slice Pos.Raw where
   hAdd p s := { byteIdx := p.byteIdx + s.utf8ByteSize }
 

src/Init/Data/String/Lemmas.lean

@@ -14,6 +14,8 @@ public import Init.Data.Char.Lemmas
 public import Init.Data.List.Lex
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
+public import Init.Data.String.Lemmas.SliceIsEmpty
+public import Init.Data.String.Lemmas.Order
 
 public section
 

src/Init/Data/String/Lemmas/Order.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Basic
+import Init.Data.String.Grind
+import Init.Data.String.Lemmas.Basic
+
+public section
+
+namespace Std
+
+theorem lt_irrefl {α : Type u} [LT α] [Std.Irrefl (α := α) (· < ·)] {a : α} : ¬ a < a :=
+  Std.Irrefl.irrefl a
+
+theorem ne_of_lt {α : Type u} [LT α] [Std.Irrefl (α := α) (· < ·)] {a b : α} : a < b → a ≠ b :=
+  fun h h' => absurd (h' ▸ h) (h' ▸ lt_irrefl)
+
+end Std
+
+namespace String
+
+@[simp]
+theorem Slice.Pos.next_le_iff_lt {s : Slice} {p q : s.Pos} {h} : p.next h ≤ q ↔ p < q :=
+  ⟨fun h => Std.lt_of_lt_of_le lt_next h, next_le_of_lt⟩
+
+@[simp]
+theorem Pos.next_le_iff_lt {s : String} {p q : s.Pos} {h} : p.next h ≤ q ↔ p < q := by
+  rw [next, Pos.ofToSlice_le_iff, ← Pos.toSlice_lt_toSlice_iff]
+  exact Slice.Pos.next_le_iff_lt
+
+@[simp]
+theorem Slice.Pos.le_startPos {s : Slice} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos :=
+  ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩
+
+@[simp]
+theorem Slice.Pos.startPos_lt_iff {s : Slice} (p : s.Pos) : s.startPos < p ↔ p ≠ s.startPos := by
+  simp [← le_startPos, Std.not_le]
+
+@[simp]
+theorem Slice.Pos.endPos_le {s : Slice} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos :=
+  ⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual⟩
+
+@[simp]
+theorem Pos.le_startPos {s : String} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos :=
+  ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩
+
+@[simp]
+theorem Pos.endPos_le {s : String} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos :=
+  ⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual⟩
+
+@[simp]
+theorem Slice.Pos.not_lt_startPos {s : Slice} {p : s.Pos} : ¬ p < s.startPos :=
+  fun h => Std.lt_irrefl (Std.lt_of_lt_of_le h (Slice.Pos.startPos_le _))
+
+theorem Slice.Pos.ne_startPos_of_lt {s : Slice} {p q : s.Pos} : p < q → q ≠ s.startPos := by
+  rintro h rfl
+  simp at h
+
+@[simp]
+theorem Slice.Pos.next_ne_startPos {s : Slice} {p : s.Pos} {h} :
+    p.next h ≠ s.startPos :=
+  ne_startPos_of_lt lt_next
+
+theorem Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff {s : Slice} {p : s.Pos}
+    {q r : (s.sliceFrom p).Pos} : Slice.Pos.ofSliceFrom q < Slice.Pos.ofSliceFrom r ↔ q < r := by
+  simp [Slice.Pos.lt_iff, Pos.Raw.lt_iff]
+
+theorem Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff {s : Slice} {p : s.Pos}
+    {q r : (s.sliceFrom p).Pos} : Slice.Pos.ofSliceFrom q ≤ Slice.Pos.ofSliceFrom r ↔ q ≤ r := by
+  simp [Slice.Pos.le_iff, Pos.Raw.le_iff]
+
+end String

src/Init/Data/String/Lemmas/SliceIsEmpty.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Basic
+import all Init.Data.String.Defs
+import Init.Data.String.Lemmas.Order
+import Init.Data.String.Lemmas.Basic
+import Init.Data.String.Grind
+import Init.Grind
+
+public section
+
+namespace String
+
+theorem Slice.isEmpty_eq {s : Slice} : s.isEmpty = (s.utf8ByteSize == 0) :=
+  (rfl)
+
+theorem Slice.isEmpty_iff {s : Slice} :
+    s.isEmpty ↔ s.utf8ByteSize = 0 := by
+  simp [Slice.isEmpty_eq]
+
+theorem Slice.startPos_eq_endPos_iff {s : Slice} :
+    s.startPos = s.endPos ↔ s.isEmpty := by
+  rw [eq_comm]
+  simp [Slice.Pos.ext_iff, Pos.Raw.ext_iff, Slice.isEmpty_iff]
+
+theorem Slice.startPos_ne_endPos_iff {s : Slice} :
+    s.startPos ≠ s.endPos ↔ s.isEmpty = false := by
+  simp [Slice.startPos_eq_endPos_iff]
+
+theorem Slice.startPos_ne_endPos {s : Slice} : s.isEmpty = false → s.startPos ≠ s.endPos :=
+  Slice.startPos_ne_endPos_iff.2
+
+theorem Slice.isEmpty_iff_eq_endPos {s : Slice} :
+    s.isEmpty ↔ ∀ (p q : s.Pos), p = q := by
+  rw [← Slice.startPos_eq_endPos_iff]
+  refine ⟨fun h p q => ?_, fun h => h _ _⟩
+  apply Std.le_antisymm
+  · apply Std.le_trans (Pos.le_endPos _) (h ▸ Pos.startPos_le _)
+  · apply Std.le_trans (Pos.le_endPos _) (h ▸ Pos.startPos_le _)
+
+theorem Slice.isEmpty_eq_false_of_lt {s : Slice} {p q : s.Pos} :
+    p < q → s.isEmpty = false := by
+  rw [← Decidable.not_imp_not]
+  simp
+  rw [Slice.isEmpty_iff_eq_endPos]
+  intro h
+  cases h p q
+  apply Std.lt_irrefl
+
+@[simp]
+theorem Slice.isEmpty_sliceFrom {s : Slice} {p : s.Pos} :
+    (s.sliceFrom p).isEmpty ↔ p = s.endPos := by
+  simp [← startPos_eq_endPos_iff, ← Pos.ofSliceFrom_inj]
+
+@[simp]
+theorem Slice.isEmpty_sliceFrom_eq_false_iff {s : Slice} {p : s.Pos} :
+    (s.sliceFrom p).isEmpty = false ↔ p ≠ s.endPos :=
+  Decidable.not_iff_not.1 (by simp)
+
+end String

src/Init/Data/String/Pattern/Basic.lean

@@ -9,6 +9,10 @@ prelude
 public import Init.Data.String.Basic
 public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Consumers.Loop
+import Init.Data.String.Lemmas.SliceIsEmpty
+import Init.Data.String.Termination
+import Init.Data.String.Grind
+import Init.Data.String.Lemmas.Order
 
 set_option doc.verso true
 
@@ -41,6 +45,77 @@ inductive SearchStep (s : Slice) where
   | matched (startPos endPos : s.Pos)
 deriving Inhabited, BEq
 
+namespace SearchStep
+
+def startPos {s : Slice} (st : SearchStep s) : s.Pos :=
+  match st with
+  | .rejected startPos _ => startPos
+  | .matched startPos _ => startPos
+
+@[simp]
+theorem startPos_rejected {s : Slice} {p q : s.Pos} : (SearchStep.rejected p q).startPos = p := (rfl)
+
+@[simp]
+theorem startPos_matched {s : Slice} {p q : s.Pos} : (SearchStep.matched p q).startPos = p := (rfl)
+
+def endPos {s : Slice} (st : SearchStep s) : s.Pos :=
+  match st with
+  | .rejected _ endPos => endPos
+  | .matched _ endPos => endPos
+
+@[simp]
+theorem endPos_rejected {s : Slice} {p q : s.Pos} : (SearchStep.rejected p q).endPos = q := (rfl)
+
+@[simp]
+theorem endPos_matched {s : Slice} {p q : s.Pos} : (SearchStep.matched p q).endPos = q := (rfl)
+
+def ofSliceFrom {s : Slice} {p : s.Pos} (st : SearchStep (s.sliceFrom p)) : SearchStep s :=
+  match st with
+  | .rejected l r => .rejected (Slice.Pos.ofSliceFrom l) (Slice.Pos.ofSliceFrom r)
+  | .matched l r => .matched (Slice.Pos.ofSliceFrom l) (Slice.Pos.ofSliceFrom r)
+
+@[simp]
+theorem startPos_ofSliceFrom {s : Slice} {p : s.Pos} {st : SearchStep (s.sliceFrom p)} :
+    st.ofSliceFrom.startPos = Slice.Pos.ofSliceFrom st.startPos := by
+  cases st <;>  simp [ofSliceFrom]
+
+@[simp]
+theorem endPos_ofSliceFrom {s : Slice} {p : s.Pos} {st : SearchStep (s.sliceFrom p)} :
+    st.ofSliceFrom.endPos = Slice.Pos.ofSliceFrom st.endPos := by
+  cases st <;> simp [ofSliceFrom]
+
+end SearchStep
+
+/--
+Provides simple pattern matching capabilities from the start of a {name}`Slice`.
+
+-/
+class ForwardPattern {ρ : Type} (pat : ρ) where
+  /--
+  Checks whether the slice starts with the pattern. If it does, the slice is returned with the
+  prefix removed; otherwise the result is {name}`none`.
+  -/
+  dropPrefix? : (s : Slice) →  Option s.Pos
+  /--
+  Checks whether the slice starts with the pattern. If it does, the slice is returned with the
+  prefix removed; otherwise the result is {name}`none`.
+  -/
+  dropPrefixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => dropPrefix? s
+  /--
+  Checks whether the slice starts with the pattern.
+  -/
+  startsWith : (s : Slice) → Bool := fun s => (dropPrefix? s).isSome
+
+class LawfulForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop where
+  dropPrefixOfNonempty?_eq {s : Slice} (h) :
+    ForwardPattern.dropPrefixOfNonempty? pat s h = ForwardPattern.dropPrefix? pat s
+  startsWith_eq (s : Slice) :
+    ForwardPattern.startsWith pat s = (ForwardPattern.dropPrefix? pat s).isSome
+
+class StrictForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop where
+  ne_startPos {s : Slice} (h) (q) :
+    ForwardPattern.dropPrefixOfNonempty? pat s h = some q → q ≠ s.startPos
+
 /--
 Provides a conversion from a pattern to an iterator of {name}`SearchStep` that searches for matches
 of the pattern from the start towards the end of a {name}`Slice`.
@@ -53,25 +128,79 @@ class ToForwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (Slice → Type))
   -/
   toSearcher : (s : Slice) → Std.Iter (α := σ s) (SearchStep s)
 
-/--
-Provides simple pattern matching capabilities from the start of a {name}`Slice`.
+namespace ToForwardSearcher
 
-While these operations can be implemented on top of {name}`ToForwardSearcher` some patterns allow
-for more efficient implementations. This class can be used to specialize for them. If there is no
-need to specialize in this fashion, then
-{name (scope := "Init.Data.String.Pattern.Basic")}`ForwardPattern.defaultImplementation` can be used
-to automatically derive an instance.
--/
-class ForwardPattern {ρ : Type} (pat : ρ) where
-  /--
-  Checks whether the slice starts with the pattern.
-  -/
-  startsWith : Slice → Bool
-  /--
-  Checks whether the slice starts with the pattern. If it does, the slice is returned with the
-  prefix removed; otherwise the result is {name}`none`.
-  -/
-  dropPrefix? : (s : Slice) → Option s.Pos
+structure DefaultForwardSearcher {ρ : Type} (pat : ρ) (s : Slice) where
+  currPos : s.Pos
+deriving Inhabited
+
+namespace DefaultForwardSearcher
+
+variable {ρ : Type} (pat : ρ)
+
+@[inline]
+def iter (s : Slice) : Std.Iter (α := DefaultForwardSearcher pat s) (SearchStep s) :=
+  ⟨⟨s.startPos⟩⟩
+
+instance (s : Slice) [ForwardPattern pat] :
+    Std.Iterator (DefaultForwardSearcher pat s) Id (SearchStep s) where
+  IsPlausibleStep it
+    | .yield it' (.rejected p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.endPos),
+      ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = none ∧
+      p₁ = it.internalState.currPos ∧ p₂ = it.internalState.currPos.next h ∧
+      it'.internalState.currPos = it.internalState.currPos.next h
+    | .yield it' (.matched p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.endPos), ∃ pos,
+      ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = some pos ∧
+      p₁ = it.internalState.currPos ∧ p₂ = Slice.Pos.ofSliceFrom pos ∧
+      it'.internalState.currPos = Slice.Pos.ofSliceFrom pos
+    | .done => it.internalState.currPos = s.endPos
+    | .skip _ => False
+  step it :=
+    if h : it.internalState.currPos = s.endPos then
+      pure (.deflate ⟨.done, by simp [h]⟩)
+    else
+      match h' : ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) with
+      | some pos =>
+        pure (.deflate ⟨.yield ⟨⟨Slice.Pos.ofSliceFrom pos⟩⟩
+          (.matched it.internalState.currPos (Slice.Pos.ofSliceFrom pos)), by simp [h, h']⟩)
+      | none =>
+        pure (.deflate ⟨.yield ⟨⟨it.internalState.currPos.next h⟩⟩
+          (.rejected it.internalState.currPos (it.internalState.currPos.next h)), by simp [h, h']⟩)
+
+def finitenessRelation (s : Slice) [ForwardPattern pat] [StrictForwardPattern pat] :
+    Std.Iterators.FinitenessRelation (DefaultForwardSearcher pat s) Id where
+  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
+  wf := InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    simp_wf
+    obtain ⟨step, h, h'⟩ := h
+    match step with
+    | .yield it'' (.rejected p₁ p₂) =>
+      obtain ⟨_, ⟨-, -, -, h'⟩⟩ := h'
+      cases h
+      simp [h']
+    | .yield it'' (.matched p₁ p₂) =>
+      obtain ⟨_, pos, ⟨h₀, -, -, h'⟩⟩ := h'
+      cases h
+      have := StrictForwardPattern.ne_startPos _ _ h₀
+      rw [h']
+      exact Std.lt_of_le_of_lt Slice.Pos.le_ofSliceFrom
+        (Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff.2 ((Slice.Pos.startPos_lt_iff _).2 this))
+
+instance {s : Slice} [ForwardPattern pat] [StrictForwardPattern pat] :
+    Std.Iterators.Finite (DefaultForwardSearcher pat s) Id :=
+  .of_finitenessRelation (finitenessRelation pat s)
+
+instance [ForwardPattern pat] : Std.IteratorLoop (DefaultForwardSearcher pat s) Id Id :=
+  .defaultImplementation
+
+end DefaultForwardSearcher
+
+@[inline]
+def defaultImplementation [ForwardPattern pat] : ToForwardSearcher pat (DefaultForwardSearcher pat) where
+  toSearcher := DefaultForwardSearcher.iter pat
+
+end ToForwardSearcher
 
 namespace Internal
 
@@ -123,33 +252,33 @@ def memcmpSlice (lhs rhs : Slice) (lstart : String.Pos.Raw) (rstart : String.Pos
 
 end Internal
 
-namespace ForwardPattern
+-- namespace ForwardPattern
 
-variable {ρ : Type} {σ : Slice → Type}
-variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
-variable (pat : ρ) [ToForwardSearcher pat σ]
+-- variable {ρ : Type} {σ : Slice → Type}
+-- variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
+-- variable (pat : ρ) [ToForwardSearcher pat σ]
 
-@[specialize pat]
-def defaultStartsWith (s : Slice) [Std.IteratorLoop (σ s) Id Id] : Bool :=
-  let searcher := ToForwardSearcher.toSearcher pat s
-  match searcher.first? with
-  | some (.matched start ..) => s.startPos = start
-  | _ => false
+-- @[specialize pat]
+-- def defaultStartsWith (s : Slice) [Std.IteratorLoop (σ s) Id Id] : Bool :=
+--   let searcher := ToForwardSearcher.toSearcher pat s
+--   match searcher.first? with
+--   | some (.matched start ..) => s.startPos = start
+--   | _ => false
 
-@[specialize pat]
-def defaultDropPrefix? (s : Slice) [Std.IteratorLoop (σ s) Id Id] : Option s.Pos :=
-  let searcher := ToForwardSearcher.toSearcher pat s
-  match searcher.first? with
-  | some (.matched _ endPos) => some endPos
-  | _ => none
+-- @[specialize pat]
+-- def defaultDropPrefix? (s : Slice) [Std.IteratorLoop (σ s) Id Id] : Option s.Pos :=
+--   let searcher := ToForwardSearcher.toSearcher pat s
+--   match searcher.first? with
+--   | some (.matched _ endPos) => some endPos
+--   | _ => none
 
-@[always_inline, inline]
-def defaultImplementation {pat : ρ} [ToForwardSearcher pat σ] [∀ s, Std.IteratorLoop (σ s) Id Id] :
-    ForwardPattern pat where
-  startsWith s := defaultStartsWith pat s
-  dropPrefix? s := defaultDropPrefix? pat s
+-- @[always_inline, inline]
+-- def defaultImplementation {pat : ρ} [ToForwardSearcher pat σ] [∀ s, Std.IteratorLoop (σ s) Id Id] :
+--     ForwardPattern pat where
+--   startsWith s := defaultStartsWith pat s
+--   dropPrefix? s := defaultDropPrefix? pat s
 
-end ForwardPattern
+-- end ForwardPattern
 
 /--
 Provides a conversion from a pattern to an iterator of {name}`SearchStep` searching for matches of

src/Init/Data/String/Pattern/Char.lean

@@ -9,6 +9,8 @@ prelude
 public import Init.Data.String.Pattern.Basic
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 import Init.Data.String.Termination
+public import Init.Data.String.Lemmas.SliceIsEmpty
+import Init.Data.String.Lemmas.Order
 
 set_option doc.verso true
 
@@ -20,68 +22,48 @@ public section
 
 namespace String.Slice.Pattern
 
-structure ForwardCharSearcher (needle : Char) (s : Slice) where
-  currPos : s.Pos
-deriving Inhabited
+namespace Char
 
-namespace ForwardCharSearcher
-
-@[inline]
-def iter (c : Char) (s : Slice) : Std.Iter (α := ForwardCharSearcher c s) (SearchStep s) :=
-  { internalState := { currPos := s.startPos }}
-
-instance (s : Slice) : Std.Iterator (ForwardCharSearcher c s) Id (SearchStep s) where
-  IsPlausibleStep it
-    | .yield it' out =>
-      ∃ h1 : it.internalState.currPos ≠ s.endPos,
-        it'.internalState.currPos = it.internalState.currPos.next h1 ∧
-        match out with
-        | .matched startPos endPos =>
-          it.internalState.currPos = startPos ∧
-          it'.internalState.currPos = endPos ∧
-          it.internalState.currPos.get h1 = c
-        | .rejected startPos endPos =>
-          it.internalState.currPos = startPos ∧
-          it'.internalState.currPos = endPos ∧
-          it.internalState.currPos.get h1 ≠ c
-    | .skip _ => False
-    | .done => it.internalState.currPos = s.endPos
-  step := fun ⟨⟨currPos⟩⟩ =>
-    if h1 : currPos = s.endPos then
-      pure (.deflate ⟨.done, by simp [h1]⟩)
+@[inline, always_inline]
+instance {c : Char} : ForwardPattern c where
+  dropPrefixOfNonempty? s h :=
+    if s.startPos.get (Slice.startPos_ne_endPos h) = c then
+      some (s.startPos.next (Slice.startPos_ne_endPos h))
     else
-      let nextPos := currPos.next h1
-      let nextIt := ⟨⟨nextPos⟩⟩
-      if h2 : currPos.get h1 = c then
-        pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
-      else
-        pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
+      none
+  dropPrefix? s :=
+    if h : s.startPos = s.endPos then
+      none
+    else if s.startPos.get h = c then
+      some (s.startPos.next h)
+    else
+      none
+  startsWith s :=
+    if h : s.startPos = s.endPos then
+      false
+    else
+      s.startPos.get h = c
 
-def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s c) Id where
-  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
-  wf := InvImage.wf _ WellFoundedRelation.wf
-  subrelation {it it'} h := by
-    simp_wf
-    obtain ⟨step, h, h'⟩ := h
-    cases step
-    · cases h
-      obtain ⟨_, h2, _⟩ := h'
-      simp [h2]
-    · cases h'
-    · cases h
+instance {c : Char} : StrictForwardPattern c where
+  ne_startPos {s h q} := by
+    simp only [ForwardPattern.dropPrefixOfNonempty?, Option.ite_none_right_eq_some,
+      Option.some.injEq, ne_eq, and_imp]
+    rintro _ rfl
+    simp
 
-instance : Std.Iterators.Finite (ForwardCharSearcher s c) Id :=
-  .of_finitenessRelation finitenessRelation
+instance {c : Char} : LawfulForwardPattern c where
+  dropPrefixOfNonempty?_eq {s h} := by
+    simp [ForwardPattern.dropPrefixOfNonempty?, ForwardPattern.dropPrefix?,
+      Slice.startPos_eq_endPos_iff, h]
+  startsWith_eq {s} := by
+    simp only [ForwardPattern.startsWith, ForwardPattern.dropPrefix?]
+    split <;> (try split) <;> simp_all
 
-instance : Std.IteratorLoop (ForwardCharSearcher s c) Id Id :=
+@[inline, always_inline]
+instance {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearcher c) :=
   .defaultImplementation
 
-instance {c : Char} : ToForwardSearcher c (ForwardCharSearcher c) where
-  toSearcher := iter c
-
-instance {c : Char} : ForwardPattern c := .defaultImplementation
-
-end ForwardCharSearcher
+end Char
 
 structure BackwardCharSearcher (s : Slice) where
   currPos : s.Pos

src/Init/Data/String/Pattern/Pred.lean

@@ -9,6 +9,8 @@ prelude
 public import Init.Data.String.Pattern.Basic
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 import Init.Data.String.Termination
+public import Init.Data.String.Lemmas.SliceIsEmpty
+import Init.Data.String.Lemmas.Order
 
 set_option doc.verso true
 
@@ -21,77 +23,63 @@ public section
 
 namespace String.Slice.Pattern
 
-structure ForwardCharPredSearcher (p : Char → Bool) (s : Slice) where
-  currPos : s.Pos
-deriving Inhabited
+namespace CharPred
 
-namespace ForwardCharPredSearcher
-
-@[inline]
-def iter (p : Char → Bool) (s : Slice) : Std.Iter (α := ForwardCharPredSearcher p s) (SearchStep s) :=
-  { internalState := { currPos := s.startPos }}
-
-instance (s : Slice) : Std.Iterator (ForwardCharPredSearcher p s) Id (SearchStep s) where
-  IsPlausibleStep it
-    | .yield it' out =>
-      ∃ h1 : it.internalState.currPos ≠ s.endPos,
-        it'.internalState.currPos = it.internalState.currPos.next h1 ∧
-        match out with
-        | .matched startPos endPos =>
-          it.internalState.currPos = startPos ∧
-          it'.internalState.currPos = endPos ∧
-          p (it.internalState.currPos.get h1)
-        | .rejected startPos endPos =>
-          it.internalState.currPos = startPos ∧
-          it'.internalState.currPos = endPos ∧
-          ¬ p (it.internalState.currPos.get h1)
-    | .skip _ => False
-    | .done => it.internalState.currPos = s.endPos
-  step := fun ⟨⟨currPos⟩⟩ =>
-    if h1 : currPos = s.endPos then
-      pure (.deflate ⟨.done, by simp [h1]⟩)
+@[default_instance]
+instance {p : Char → Bool} : ForwardPattern p where
+  dropPrefixOfNonempty? s h :=
+    if p (s.startPos.get (Slice.startPos_ne_endPos h)) then
+      some (s.startPos.next (Slice.startPos_ne_endPos h))
     else
-      let nextPos := currPos.next h1
-      let nextIt := ⟨⟨nextPos⟩⟩
-      if h2 : p <| currPos.get h1 then
-        pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
-      else
-        pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
+      none
+  dropPrefix? s :=
+    if h : s.startPos = s.endPos then
+      none
+    else if p (s.startPos.get h) then
+      some (s.startPos.next h)
+    else
+      none
+  startsWith s :=
+    if h : s.startPos = s.endPos then
+      false
+    else
+      p (s.startPos.get h)
 
+instance {p : Char → Bool} : StrictForwardPattern p where
+  ne_startPos {s h q} := by
+    simp only [ForwardPattern.dropPrefixOfNonempty?, Option.ite_none_right_eq_some,
+      Option.some.injEq, ne_eq, and_imp]
+    rintro _ rfl
+    simp
 
-def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher p s) Id where
-  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
-  wf := InvImage.wf _ WellFoundedRelation.wf
-  subrelation {it it'} h := by
-    simp_wf
-    obtain ⟨step, h, h'⟩ := h
-    cases step
-    · cases h
-      obtain ⟨_, h2, _⟩ := h'
-      simp [h2]
-    · cases h'
-    · cases h
-
-instance : Std.Iterators.Finite (ForwardCharPredSearcher p s) Id :=
-  .of_finitenessRelation finitenessRelation
-
-instance : Std.IteratorLoop (ForwardCharPredSearcher p s) Id Id :=
-  .defaultImplementation
+instance {p : Char → Bool} : LawfulForwardPattern p where
+  dropPrefixOfNonempty?_eq {s} h := by
+    simp [ForwardPattern.dropPrefixOfNonempty?, ForwardPattern.dropPrefix?,
+      Slice.startPos_eq_endPos_iff, h]
+  startsWith_eq s := by
+    simp only [ForwardPattern.startsWith, ForwardPattern.dropPrefix?]
+    split <;> (try split) <;> simp_all
 
 @[default_instance]
-instance {p : Char → Bool} : ToForwardSearcher p (ForwardCharPredSearcher p) where
-  toSearcher := iter p
-
-@[default_instance]
-instance {p : Char → Bool} : ForwardPattern p := .defaultImplementation
-
-instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ForwardCharPredSearcher p) where
-  toSearcher := iter (decide <| p ·)
-
-instance {p : Char → Prop} [DecidablePred p] : ForwardPattern p :=
+instance {p : Char → Bool} : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher p) :=
   .defaultImplementation
 
-end ForwardCharPredSearcher
+instance {p : Char → Prop} [DecidablePred p] : ForwardPattern p where
+  dropPrefixOfNonempty? s h := ForwardPattern.dropPrefixOfNonempty? (decide <| p ·) s h
+  dropPrefix? s := ForwardPattern.dropPrefix? (decide <| p ·) s
+  startsWith s := ForwardPattern.startsWith (decide <| p ·) s
+
+instance {p : Char → Prop} [DecidablePred p] : StrictForwardPattern p where
+  ne_startPos h q := StrictForwardPattern.ne_startPos (pat := (decide <| p ·)) h q
+
+instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPattern p where
+  dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (decide <| p ·)) h
+  startsWith_eq s := LawfulForwardPattern.startsWith_eq (pat := (decide <| p ·)) s
+
+instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher p) :=
+  .defaultImplementation
+
+end CharPred
 
 structure BackwardCharPredSearcher (s : Slice) where
   currPos : s.Pos

src/Init/Data/String/Positions.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving, Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Basic
+public import Init.Data.Iterators.Consumers.Monadic.Loop
+import Init.Data.Iterators.Combinators.FilterMap
+import Init.Data.String.Termination
+
+set_option doc.verso true
+
+public section
+
+namespace String.Slice
+
+structure PosIterator (s : Slice) where
+  currPos : s.Pos
+deriving Inhabited
+
+set_option doc.verso false
+/--
+Creates an iterator over all valid positions within {name}`s`.
+Examples
+ * {lean}`("abc".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', 'c']`
+ * {lean}`("abc".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2]`
+ * {lean}`("ab∀c".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', '∀', 'c']`
+ * {lean}`("ab∀c".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2, 5]`
+-/
+def positions (s : Slice) : Std.Iter (α := PosIterator s) { p : s.Pos // p ≠ s.endPos } :=
+  { internalState := { currPos := s.startPos }}
+
+set_option doc.verso true
+
+namespace PosIterator
+
+instance : Std.Iterator (PosIterator s) Id { p : s.Pos // p ≠ s.endPos } where
+  IsPlausibleStep it
+    | .yield it' out =>
+      ∃ h : it.internalState.currPos ≠ s.endPos,
+        it'.internalState.currPos = it.internalState.currPos.next h ∧
+        it.internalState.currPos = out
+    | .skip _ => False
+    | .done => it.internalState.currPos = s.endPos
+  step := fun ⟨⟨currPos⟩⟩ =>
+    if h : currPos = s.endPos then
+      pure (.deflate ⟨.done, by simp [h]⟩)
+    else
+      pure (.deflate ⟨.yield ⟨⟨currPos.next h⟩⟩ ⟨currPos, h⟩, by simp [h]⟩)
+
+private def finitenessRelation :
+    Std.Iterators.FinitenessRelation (PosIterator s) Id where
+  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
+  wf := InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    simp_wf
+    obtain ⟨step, h, h'⟩ := h
+    cases step
+    · cases h
+      obtain ⟨_, h2, _⟩ := h'
+      simp [h2]
+    · cases h'
+    · cases h
+
+@[no_expose]
+instance : Std.Iterators.Finite (PosIterator s) Id :=
+  .of_finitenessRelation finitenessRelation
+
+instance : Std.IteratorLoop (PosIterator s) Id Id :=
+  .defaultImplementation
+
+docs_to_verso positions
+
+end PosIterator
+
+structure RevPosIterator (s : Slice) where
+  currPos : s.Pos
+deriving Inhabited
+
+set_option doc.verso false
+/--
+Creates an iterator over all valid positions within {name}`s`, starting from the last valid
+position and iterating towards the first one.
+Examples
+ * {lean}`("abc".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', 'b', 'a']`
+ * {lean}`("abc".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [2, 1, 0]`
+ * {lean}`("ab∀c".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', '∀', 'b', 'a']`
+ * {lean}`("ab∀c".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [5, 2, 1, 0]`
+-/
+def revPositions (s : Slice) : Std.Iter (α := RevPosIterator s) { p : s.Pos // p ≠ s.endPos } :=
+  { internalState := { currPos := s.endPos }}
+
+set_option doc.verso true
+
+namespace RevPosIterator
+
+instance [Pure m] :
+    Std.Iterator (RevPosIterator s) m { p : s.Pos // p ≠ s.endPos } where
+  IsPlausibleStep it
+    | .yield it' out =>
+      ∃ h : it.internalState.currPos ≠ s.startPos,
+        it'.internalState.currPos = it.internalState.currPos.prev h ∧
+        it.internalState.currPos.prev h = out
+    | .skip _ => False
+    | .done => it.internalState.currPos = s.startPos
+  step := fun ⟨⟨currPos⟩⟩ =>
+    if h : currPos = s.startPos then
+      pure (.deflate ⟨.done, by simp [h]⟩)
+    else
+      let prevPos := currPos.prev h
+      pure (.deflate ⟨.yield ⟨⟨prevPos⟩⟩ ⟨prevPos, Pos.prev_ne_endPos⟩, by simp [h, prevPos]⟩)
+
+private def finitenessRelation [Pure m] :
+    Std.Iterators.FinitenessRelation (RevPosIterator s) m where
+  Rel := InvImage WellFoundedRelation.rel
+      (fun it => it.internalState.currPos.down)
+  wf := InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    simp_wf
+    obtain ⟨step, h, h'⟩ := h
+    cases step
+    · cases h
+      obtain ⟨h1, h2, _⟩ := h'
+      simp [h2]
+    · cases h'
+    · cases h
+
+@[no_expose]
+instance [Pure m] : Std.Iterators.Finite (RevPosIterator s) m :=
+  .of_finitenessRelation finitenessRelation
+
+instance [Monad m] [Monad n] : Std.IteratorLoop (RevPosIterator s) m n :=
+  .defaultImplementation
+
+docs_to_verso revPositions
+
+end RevPosIterator
+
+
+end String.Slice

src/Init/Data/String/Slice.lean

@@ -11,6 +11,8 @@ public import Init.Data.Ord.Basic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Termination
+public import Init.Data.String.Subslice
+public import Init.Data.String.Positions
 
 set_option doc.verso true
 
@@ -46,18 +48,6 @@ instance : HAppend String String.Slice String where
 
 open Pattern
 
-/--
-Checks whether a slice is empty.
-
-Empty slices have {name}`utf8ByteSize` {lean}`0`.
-
-Examples:
- * {lean}`"".toSlice.isEmpty = true`
- * {lean}`" ".toSlice.isEmpty = false`
--/
-@[inline]
-def isEmpty (s : Slice) : Bool := s.utf8ByteSize == 0
-
 /--
 Checks whether {name}`s1` and {name}`s2` represent the same string, even if they are slices of
 different base strings or different slices within the same string.
@@ -97,6 +87,13 @@ instance : LE Slice where
 instance : DecidableLE Slice :=
   fun x y => inferInstanceAs (Decidable (¬x < y))
 
+namespace Subslice
+
+instance {s : Slice} : BEq s.Subslice where
+  beq sl sl' := sl.toSlice == sl'.toSlice
+
+end Subslice
+
 section ForwardPatternUsers
 
 variable {ρ : Type} {σ : Slice → Type}
@@ -131,7 +128,7 @@ variable {pat : ρ} [ToForwardSearcher pat σ]
 
 inductive PlausibleStep
 
-instance : Std.Iterator (SplitIterator pat s) Id Slice where
+instance : Std.Iterator (SplitIterator pat s) Id s.Subslice where
   IsPlausibleStep
     | ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
     | ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
@@ -145,7 +142,7 @@ instance : Std.Iterator (SplitIterator pat s) Id Slice where
     | ⟨.operating currPos searcher⟩ =>
       match h : searcher.step with
       | ⟨.yield searcher' (.matched startPos endPos), hps⟩ =>
-        let slice := s.slice! currPos startPos
+        let slice := s.subslice! currPos startPos
         let nextIt := ⟨.operating endPos searcher'⟩
         pure (.deflate ⟨.yield nextIt slice, by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
       | ⟨.yield searcher' (.rejected ..), hps⟩ =>
@@ -155,7 +152,7 @@ instance : Std.Iterator (SplitIterator pat s) Id Slice where
         pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
           by simp [hps.isPlausibleSuccessor_of_skip]⟩)
       | ⟨.done, _⟩ =>
-        let slice := s.sliceFrom currPos
+        let slice := s.subsliceFrom currPos
         pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
     | ⟨.atEnd⟩ => pure (.deflate ⟨.done, by simp⟩)
 
@@ -190,6 +187,11 @@ instance [Monad n] : Std.IteratorLoop (SplitIterator pat s) Id n :=
 
 end SplitIterator
 
+@[specialize pat]
+def splitToSubslice (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] :
+    Std.Iter (α := SplitIterator pat s) s.Subslice :=
+  { internalState := .operating s.startPos (ToForwardSearcher.toSearcher pat s) }
+
 /--
 Splits a slice at each subslice that matches the pattern {name}`pat`.
 
@@ -205,9 +207,9 @@ Examples:
  * {lean}`("ababababa".toSlice.split "aba").toList == ["coffee".toSlice, "water".toSlice]`
  * {lean}`("baaab".toSlice.split "aa").toList == ["b".toSlice, "ab".toSlice]`
 -/
-@[specialize pat]
-def split (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] : Std.Iter (α := SplitIterator pat s) Slice :=
-  { internalState := .operating s.startPos (ToForwardSearcher.toSearcher pat s) }
+@[inline]
+def split (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] :=
+  (s.splitToSubslice pat |>.map Subslice.toSlice : Std.Iter Slice)
 
 inductive SplitInclusiveIterator {ρ : Type} (pat : ρ) (s : Slice) [ToForwardSearcher pat σ] where
   | operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
@@ -218,7 +220,7 @@ namespace SplitInclusiveIterator
 
 variable {pat : ρ} [ToForwardSearcher pat σ]
 
-instance : Std.Iterator (SplitInclusiveIterator pat s) Id Slice where
+instance : Std.Iterator (SplitInclusiveIterator pat s) Id s.Subslice where
   IsPlausibleStep
     | ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
     | ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
@@ -232,7 +234,7 @@ instance : Std.Iterator (SplitInclusiveIterator pat s) Id Slice where
     | ⟨.operating currPos searcher⟩ =>
       match h : searcher.step with
       | ⟨.yield searcher' (.matched _ endPos), hps⟩ =>
-        let slice := s.slice! currPos endPos
+        let slice := s.subslice! currPos endPos
         let nextIt := ⟨.operating endPos searcher'⟩
         pure (.deflate ⟨.yield nextIt slice,
           by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
@@ -244,7 +246,7 @@ instance : Std.Iterator (SplitInclusiveIterator pat s) Id Slice where
           by simp [hps.isPlausibleSuccessor_of_skip]⟩)
       | ⟨.done, _⟩ =>
         if currPos != s.endPos then
-          let slice := s.sliceFrom currPos
+          let slice := s.subsliceFrom currPos
           pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
         else
           pure (.deflate ⟨.done, by simp⟩)
@@ -283,6 +285,11 @@ instance [Monad n] {s} :
 
 end SplitInclusiveIterator
 
+@[specialize pat]
+def splitToSubsliceInclusive (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] :
+    Std.Iter (α := SplitInclusiveIterator pat s) s.Subslice :=
+  { internalState := .operating s.startPos (ToForwardSearcher.toSearcher pat s) }
+
 /--
 Splits a slice at each subslice that matches the pattern {name}`pat`. Unlike {name}`split` the
 matched subslices are included at the end of each subslice.
@@ -295,10 +302,9 @@ Examples:
  * {lean}`("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]`
  * {lean}`("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]`
 -/
-@[specialize pat]
-def splitInclusive (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] :
-    Std.Iter (α := SplitInclusiveIterator pat s) Slice :=
-  { internalState := .operating s.startPos (ToForwardSearcher.toSearcher pat s) }
+@[inline]
+def splitInclusive (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] :=
+  (s.splitToSubsliceInclusive pat |>.map Subslice.toSlice : Std.Iter Slice)
 
 /--
 If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
@@ -829,71 +835,6 @@ where
     simp [String.Pos.Raw.lt_iff] at h ⊢
     omega
 
-structure PosIterator (s : Slice) where
-  currPos : s.Pos
-deriving Inhabited
-
-set_option doc.verso false
-/--
-Creates an iterator over all valid positions within {name}`s`.
-
-Examples
- * {lean}`("abc".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', 'c']`
- * {lean}`("abc".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2]`
- * {lean}`("ab∀c".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', '∀', 'c']`
- * {lean}`("ab∀c".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2, 5]`
--/
-def positions (s : Slice) : Std.Iter (α := PosIterator s) { p : s.Pos // p ≠ s.endPos } :=
-  { internalState := { currPos := s.startPos }}
-
-set_option doc.verso true
-
-namespace PosIterator
-
-instance [Pure m] :
-    Std.Iterator (PosIterator s) m { p : s.Pos // p ≠ s.endPos } where
-  IsPlausibleStep it
-    | .yield it' out =>
-      ∃ h : it.internalState.currPos ≠ s.endPos,
-        it'.internalState.currPos = it.internalState.currPos.next h ∧
-        it.internalState.currPos = out
-    | .skip _ => False
-    | .done => it.internalState.currPos = s.endPos
-  step := fun ⟨⟨currPos⟩⟩ =>
-    if h : currPos = s.endPos then
-      pure (.deflate ⟨.done, by simp [h]⟩)
-    else
-      pure (.deflate ⟨.yield ⟨⟨currPos.next h⟩⟩ ⟨currPos, h⟩, by simp [h]⟩)
-
-private def finitenessRelation [Pure m] :
-    Std.Iterators.FinitenessRelation (PosIterator s) m where
-  Rel := InvImage WellFoundedRelation.rel
-      (fun it => s.utf8ByteSize - it.internalState.currPos.offset.byteIdx)
-  wf := InvImage.wf _ WellFoundedRelation.wf
-  subrelation {it it'} h := by
-    simp_wf
-    obtain ⟨step, h, h'⟩ := h
-    cases step
-    · cases h
-      obtain ⟨h1, h2, _⟩ := h'
-      have h3 := Char.utf8Size_pos (it.internalState.currPos.get h1)
-      have h4 := it.internalState.currPos.isValidForSlice.le_utf8ByteSize
-      simp [Pos.ext_iff, String.Pos.Raw.ext_iff] at h1 h2 h4
-      omega
-    · cases h'
-    · cases h
-
-@[no_expose]
-instance [Pure m] : Std.Iterators.Finite (PosIterator s) m :=
-  .of_finitenessRelation finitenessRelation
-
-instance [Monad m] [Monad n] : Std.IteratorLoop (PosIterator s) m n :=
-  .defaultImplementation
-
-docs_to_verso positions
-
-end PosIterator
-
 /--
 Creates an iterator over all characters (Unicode code points) in {name}`s`.
 
@@ -909,72 +850,6 @@ def chars (s : Slice) :=
 def length (s : Slice) : Nat :=
   s.positions.count
 
-structure RevPosIterator (s : Slice) where
-  currPos : s.Pos
-deriving Inhabited
-
-set_option doc.verso false
-/--
-Creates an iterator over all valid positions within {name}`s`, starting from the last valid
-position and iterating towards the first one.
-
-Examples
- * {lean}`("abc".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', 'b', 'a']`
- * {lean}`("abc".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [2, 1, 0]`
- * {lean}`("ab∀c".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', '∀', 'b', 'a']`
- * {lean}`("ab∀c".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [5, 2, 1, 0]`
--/
-def revPositions (s : Slice) : Std.Iter (α := RevPosIterator s) { p : s.Pos // p ≠ s.endPos } :=
-  { internalState := { currPos := s.endPos }}
-
-set_option doc.verso true
-
-namespace RevPosIterator
-
-instance [Pure m] :
-    Std.Iterator (RevPosIterator s) m { p : s.Pos // p ≠ s.endPos } where
-  IsPlausibleStep it
-    | .yield it' out =>
-      ∃ h : it.internalState.currPos ≠ s.startPos,
-        it'.internalState.currPos = it.internalState.currPos.prev h ∧
-        it.internalState.currPos.prev h = out
-    | .skip _ => False
-    | .done => it.internalState.currPos = s.startPos
-  step := fun ⟨⟨currPos⟩⟩ =>
-    if h : currPos = s.startPos then
-      pure (.deflate ⟨.done, by simp [h]⟩)
-    else
-      let prevPos := currPos.prev h
-      pure (.deflate ⟨.yield ⟨⟨prevPos⟩⟩ ⟨prevPos, Pos.prev_ne_endPos⟩, by simp [h, prevPos]⟩)
-
-private def finitenessRelation [Pure m] :
-    Std.Iterators.FinitenessRelation (RevPosIterator s) m where
-  Rel := InvImage WellFoundedRelation.rel
-      (fun it => it.internalState.currPos.offset.byteIdx)
-  wf := InvImage.wf _ WellFoundedRelation.wf
-  subrelation {it it'} h := by
-    simp_wf
-    obtain ⟨step, h, h'⟩ := h
-    cases step
-    · cases h
-      obtain ⟨h1, h2, _⟩ := h'
-      have h3 := Pos.offset_prev_lt_offset (h := h1)
-      simp [Pos.ext_iff, String.Pos.Raw.ext_iff, String.Pos.Raw.lt_iff] at h2 h3
-      omega
-    · cases h'
-    · cases h
-
-@[no_expose]
-instance [Pure m] : Std.Iterators.Finite (RevPosIterator s) m :=
-  .of_finitenessRelation finitenessRelation
-
-instance [Monad m] [Monad n] : Std.IteratorLoop (RevPosIterator s) m n :=
-  .defaultImplementation
-
-docs_to_verso revPositions
-
-end RevPosIterator
-
 /--
 Creates an iterator over all characters (Unicode code points) in {name}`s`, starting from the end
 of the slice and iterating towards the start.

src/Init/Data/String/Subslice.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Basic
+import Init.Data.String.Termination
+import Init.Data.String.Lemmas.Basic
+import Init.Data.String.Lemmas.Order
+import Init.Data.String.Grind
+
+public section
+
+namespace String.Slice
+
+/--
+A region or slice of a slice.
+-/
+@[ext]
+structure Subslice (s : Slice) where
+  /-- The byte position of the start of the subslice. -/
+  startInclusive : s.Pos
+  /-- The byte position of the end of the subslice. -/
+  endExclusive : s.Pos
+  /-- The subslice is not degenerate (but it may be empty). -/
+  startInclusive_le_endExclusive : startInclusive ≤ endExclusive
+
+instance {s : Slice} : Inhabited s.Subslice where
+  default := ⟨s.endPos, s.endPos, by exact Slice.Pos.le_refl _⟩
+
+namespace Subslice
+
+/-- Turns a subslice into a standalone slice. -/
+@[inline, expose] -- for the defeq `sl.toSlice.str = s.str`.
+def toSlice {s : Slice} (sl : s.Subslice) : Slice :=
+  s.slice sl.startInclusive sl.endExclusive sl.startInclusive_le_endExclusive
+
+@[simp]
+theorem str_toSlice {s : Slice} {sl : s.Subslice} : sl.toSlice.str = s.str := rfl
+
+@[simp]
+theorem startInclusive_toSlice {s : Slice} {sl : s.Subslice} :
+    sl.toSlice.startInclusive = sl.startInclusive.str := rfl
+
+@[simp]
+theorem endExclusive_toSlice {s : Slice} {sl : s.Subslice} :
+    sl.toSlice.endExclusive = sl.endExclusive.str := rfl
+
+end Subslice
+
+/-- Constructs a subslice of `s`. -/
+@[inline]
+def subslice (s : Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd) : s.Subslice where
+  startInclusive := newStart
+  endExclusive := newEnd
+  startInclusive_le_endExclusive := h
+
+@[simp]
+theorem toSlice_subslice {s : Slice} {newStart newEnd h} :
+    (s.subslice newStart newEnd h).toSlice = s.slice newStart newEnd h := (rfl)
+
+@[simp]
+theorem startInclusive_subslice {s : Slice} {newStart newEnd : s.Pos} {h} :
+    (s.subslice newStart newEnd h).startInclusive = newStart := (rfl)
+
+@[simp]
+theorem endExclusive_subslice {s : Slice} {newStart newEnd : s.Pos} {h} :
+    (s.subslice newStart newEnd h).endExclusive = newEnd := (rfl)
+
+def subslice! (s : Slice) (newStart newEnd : s.Pos) : s.Subslice :=
+  if h : newStart ≤ newEnd then s.subslice _ _ h else panic! "Trying to construct a degenerate subslice"
+
+/-- Constructs a subslice of `s` starting at the given position and going until the end of the slice. -/
+@[inline]
+def subsliceFrom (s : Slice) (newStart : s.Pos) : s.Subslice :=
+  s.subslice newStart s.endPos (Slice.Pos.le_endPos _)
+
+@[simp]
+theorem startInclusive_subsliceFrom {s : Slice} {newStart : s.Pos} :
+    (s.subsliceFrom newStart).startInclusive = newStart := (rfl)
+
+@[simp]
+theorem endExclusive_subsliceFrom {s : Slice} {newStart : s.Pos} :
+    (s.subsliceFrom newStart).endExclusive = s.endPos := (rfl)
+
+/-- The entire slice, as a subslice of itself. -/
+@[inline]
+def toSubslice (s : Slice) : s.Subslice :=
+  s.subslice s.startPos s.endPos (Slice.Pos.le_endPos _)
+
+namespace Subslice
+
+def ofSliceFrom {s : Slice} {p : s.Pos} (sl : (s.sliceFrom p).Subslice) : s.Subslice where
+  startInclusive := Slice.Pos.ofSliceFrom sl.startInclusive
+  endExclusive := Slice.Pos.ofSliceFrom sl.endExclusive
+  startInclusive_le_endExclusive := Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff.2 sl.startInclusive_le_endExclusive
+
+@[simp]
+theorem startInclusive_ofSliceFrom {s : Slice} {p : s.Pos} {sl : (s.sliceFrom p).Subslice} :
+    sl.ofSliceFrom.startInclusive = Slice.Pos.ofSliceFrom sl.startInclusive := (rfl)
+
+@[simp]
+theorem endExclusive_ofSliceFrom {s : Slice} {p : s.Pos} {sl : (s.sliceFrom p).Subslice} :
+    sl.ofSliceFrom.endExclusive = Slice.Pos.ofSliceFrom sl.endExclusive := (rfl)
+
+@[simp]
+
+def extendLeft {s : Slice} {sl : s.Subslice} (newStart : s.Pos) (h : newStart ≤ sl.startInclusive) : s.Subslice where
+  startInclusive := newStart
+  endExclusive := sl.endExclusive
+  startInclusive_le_endExclusive := Std.le_trans h sl.startInclusive_le_endExclusive
+
+@[simp]
+theorem startInclusive_extendLeft {s : Slice} {sl : s.Subslice} {newStart : s.Pos} {h} :
+    (sl.extendLeft newStart h).startInclusive = newStart := (rfl)
+
+@[simp]
+theorem endExclusive_extendLeft {s : Slice} {sl : s.Subslice} {newStart : s.Pos} {h} :
+    (sl.extendLeft newStart h).endExclusive = sl.endExclusive := (rfl)
+
+def cast {s t : Slice} (h : s = t) (sl : s.Subslice) : t.Subslice where
+  startInclusive := sl.startInclusive.cast h
+  endExclusive := sl.endExclusive.cast h
+  startInclusive_le_endExclusive := by simpa using sl.startInclusive_le_endExclusive
+
+@[simp]
+theorem startInclusive_cast {s t : Slice} {h : s = t} {sl : s.Subslice} :
+    (sl.cast h).startInclusive = sl.startInclusive.cast h := (rfl)
+
+@[simp]
+theorem endExclusive_cast {s t : Slice} {h : s = t} {sl : s.Subslice} :
+    (sl.cast h).endExclusive = sl.endExclusive.cast h := (rfl)
+
+@[simp]
+theorem cast_rfl {s : Slice} : Subslice.cast (s := s) rfl = id := by
+  ext <;> simp
+
+end Subslice
+
+end String.Slice

src/Init/Data/String/Termination.lean

@@ -103,6 +103,17 @@ theorem le_refl {s : Slice} (p : s.Pos) : p ≤ p := by
 theorem lt_trans {s : Slice} {p q r : s.Pos} : p < q → q < r → p < r := by
   simpa [Pos.lt_iff, Pos.Raw.lt_iff] using Nat.lt_trans
 
+theorem le_of_lt {s : Slice} {p q : s.Pos} : p < q → p ≤ q := by
+  simpa [Pos.lt_iff, Pos.le_iff, Pos.Raw.lt_iff, Pos.Raw.le_iff] using Nat.le_of_lt
+
+@[simp]
+theorem Slice.Pos.le_next {s : Slice} {p : s.Pos} {h} : p ≤ p.next h :=
+  le_of_lt Pos.lt_next
+
+@[simp]
+theorem Slice.Pos.prev_le {s : Slice} {p : s.Pos} {h} : p.prev h ≤ p :=
+  le_of_lt Pos.prev_lt
+
 @[simp]
 theorem lt_next_next {s : Slice} {p : s.Pos} {h h'} : p < (p.next h).next h' :=
   lt_trans p.lt_next (p.next h).lt_next

src/Init/System/Uri.lean

@@ -110,13 +110,11 @@ def fileUriToPath? (uri : String) : Option System.FilePath := Id.run do
   else
     let mut p := (unescapeUri uri).drop "file://".length |>.copy
     p := p.dropWhile (λ c => c != '/') |>.copy -- drop the hostname.
-    if System.Platform.isWindows then
-      -- On Windows, the path "/c:/temp" needs to become "C:/temp"
-      if p.length >= 2 &&
-          p.front == '/' && (String.Pos.Raw.get p ⟨1⟩).isAlpha && String.Pos.Raw.get p ⟨2⟩ == ':' then
-        -- see also `pathToUri`
-        p := String.Pos.Raw.modify (p.drop 1).copy 0 .toUpper
-      p := p.map (fun c => if c == '/' then '\\' else c)
+    -- On Windows, the path "/c:/temp" needs to become "C:/temp"
+    if System.Platform.isWindows && p.length >= 2 &&
+        p.front == '/' && (String.Pos.Raw.get p ⟨1⟩).isAlpha && String.Pos.Raw.get p ⟨2⟩ == ':' then
+      -- see also `pathToUri`
+      p := String.Pos.Raw.modify (p.drop 1).copy 0 .toUpper
     some p
 
 end Uri

src/Lean/Server/Test/Runner.lean

@@ -265,26 +265,26 @@ def ident : Parser Name := do
   return xs.foldl .str $ .mkSimple head
 
 def patchUri (s : String) : IO String := do
-  let patterns := #["/src/Init/", "/src/Lean/", "/src/Std/", "/tests/lean/interactive/"]
   let some path := System.Uri.fileUriToPath? s
     | return s
-  let path ← try
-    IO.FS.realPath path
-  catch _ =>
+  let path ←
+    try
+      IO.FS.realPath path
+    catch _ =>
+      return s
+  let c := path.components.toArray
+  if let some (_, srcIdx) := c.zipIdx.filter (·.1 == "src") |>.back? then
+    if ! c[srcIdx + 1]?.any (fun dir => dir == "Init" || dir == "Lean" || dir == "Std") then
+      return s
+    let c := c.drop <| srcIdx
+    let path := System.mkFilePath c.toList
+    return System.Uri.pathToUri path
+  if let some (_, testIdx) := c.zipIdx.filter (·.1 == "tests") |>.back? then
+    let c := c.drop <| testIdx
+    let path := System.mkFilePath c.toList
+    return System.Uri.pathToUri path
+  else
     return s
-  let path := String.intercalate "/" path.components |>.toSlice
-  let matchPositions := patterns.filterMap fun p =>
-    String.Slice.Pattern.ToForwardSearcher.toSearcher p path
-      |>.filterMap (fun | .matched startPos _ => some startPos | .rejected .. => none)
-      |>.toArray.back?
-  let deepestMatchPos := matchPositions.foldr (init := path.startPos) fun matchPos deepestMatchPos =>
-    if matchPos > deepestMatchPos then
-      matchPos
-    else
-      deepestMatchPos
-  let path := path.sliceFrom deepestMatchPos
-  let path := System.FilePath.mk path.toString |>.normalize
-  return System.Uri.pathToUri path
 
 partial def patchUris : Json → IO Json
   | .null =>