chore: expose Substring.prev/next

src/Init/Data/String/Basic.lean

@@ -345,23 +345,23 @@ namespace Substring
 
 /-- Given an offset of a codepoint into the substring,
 return the offset there of the next codepoint. -/
-@[inline] private def next : Substring → String.Pos → String.Pos
+@[inline] def next : Substring → String.Pos → String.Pos
   | ⟨s, b, e⟩, p =>
     let absP := b+p
     if absP = e then p else s.next absP - b
 
 /-- Given an offset of a codepoint into the substring,
 return the offset there of the previous codepoint. -/
-@[inline] private def prev : Substring → String.Pos → String.Pos
+@[inline] def prev : Substring → String.Pos → String.Pos
   | ⟨s, b, _⟩, p =>
     let absP := b+p
     if absP = b then p else s.prev absP - b
 
-private def nextn : Substring → Nat → String.Pos → String.Pos
+def nextn : Substring → Nat → String.Pos → String.Pos
   | ss, 0,   p => p
   | ss, i+1, p => ss.nextn i (ss.next p)
 
-private def prevn : Substring → String.Pos → Nat → String.Pos
+def prevn : Substring → String.Pos → Nat → String.Pos
   | ss, 0,   p => p
   | ss, i+1, p => ss.prevn i (ss.prev p)
 
@@ -390,7 +390,7 @@ or `s.bsize` if `c` doesn't occur. -/
   | ⟨s, b, e⟩, p => b + p == e
 
 @[inline] def extract : Substring → String.Pos → String.Pos → Substring
-  | ⟨s, b, _⟩, b', e' => if b' ≥ e' then ⟨"", 0, 1⟩ else ⟨s, b+b', b+e'⟩
+  | ⟨s, b, e⟩, b', e' => if b' ≥ e' then ⟨"", 0, 0⟩ else ⟨s, e.min (b+b'), e.min (b+e')⟩
 
 partial def splitOn (s : Substring) (sep : String := " ") : List Substring :=
   if sep == "" then