From caa8f7f7b2b3c1456c8f73f83030746f4be9d1bf Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 18 Jul 2021 15:41:04 -0700 Subject: [PATCH] chore: expose Substring.prev/next --- src/Init/Data/String/Basic.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 344cd9a7f0..81ac8a245e 100644 --- a/src/Init/Data/String/Basic.lean +++ b/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