diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 9655ff6474..d99698549f 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1104,7 +1104,7 @@ def Slice.slice? (s : Slice) (newStart newEnd : s.Pos) : Option Slice := /-- Given a slice and two valid positions within the slice, obtain a new slice on the same underlying string formed by the new bounds, or panic if the given end is strictly less than the given start. -/ def Slice.slice! (s : Slice) (newStart newEnd : s.Pos) : Slice := - if h : newStart.offset ≤ newEnd.offset then + if h : newStart ≤ newEnd then s.slice newStart newEnd h else panic! "Starting position must be less than or equal to end position." @@ -1219,12 +1219,12 @@ theorem Pos.offset_toSlice {s : String} {pos : s.Pos} : pos.toSlice.offset = pos /-- Given a string `s`, turns a valid position on the slice `s.toSlice` into a valid position on the string `s`. -/ @[inline, expose] -def Slice.Pos.ofSlice {s : String} (pos : s.toSlice.Pos) : s.Pos where +def Pos.ofToSlice {s : String} (pos : s.toSlice.Pos) : s.Pos where offset := pos.offset isValid := pos.isValidForSlice.ofSlice @[simp] -theorem Slice.Pos.offset_ofSlice {s : String} {pos : s.toSlice.Pos} : pos.ofSlice.offset = pos.offset := (rfl) +theorem Pos.offset_ofToSlice {s : String} {pos : s.toSlice.Pos} : (ofToSlice pos).offset = pos.offset := (rfl) @[simp] theorem rawEndPos_toSlice {s : String} : s.toSlice.rawEndPos = s.rawEndPos := by @@ -1239,25 +1239,25 @@ theorem startPos_toSlice {s : String} : s.toSlice.startPos = s.startPos.toSlice Slice.Pos.ext (by simp) @[simp] -theorem Pos.ofSlice_toSlice {s : String} (pos : s.Pos) : pos.toSlice.ofSlice = pos := +theorem Pos.ofToSlice_toSlice {s : String} (pos : s.Pos) : (ofToSlice pos.toSlice) = pos := Pos.ext (by simp) @[simp] -theorem Slice.Pos.toSlice_ofSlice {s : String} (pos : s.toSlice.Pos) : pos.ofSlice.toSlice = pos := +theorem Slice.Pos.toSlice_ofToSlice {s : String} (pos : s.toSlice.Pos) : (Pos.ofToSlice pos).toSlice = pos := Slice.Pos.ext (by simp) @[simp] -theorem Slice.Pos.toSlice_comp_ofSlice {s : String} : - Pos.toSlice ∘ (ofSlice (s := s)) = id := by ext; simp +theorem Pos.toSlice_comp_ofToSlice {s : String} : + Pos.toSlice ∘ (Pos.ofToSlice (s := s)) = id := by ext; simp @[simp] -theorem Pos.ofSlice_comp_toSlice {s : String} : - Slice.Pos.ofSlice ∘ (toSlice (s := s)) = id := by ext; simp +theorem Pos.ofToSlice_comp_toSlice {s : String} : + Pos.ofToSlice ∘ (toSlice (s := s)) = id := by ext; simp theorem Pos.toSlice_inj {s : String} {p q : s.Pos} : p.toSlice = q.toSlice ↔ p = q := - ⟨fun h => by simpa using congrArg Slice.Pos.ofSlice h, (· ▸ rfl)⟩ + ⟨fun h => by simpa using congrArg Pos.ofToSlice h, (· ▸ rfl)⟩ -theorem Slice.Pos.ofSlice_inj {s : String} {p q : s.toSlice.Pos} : p.ofSlice = q.ofSlice ↔ p = q := +theorem Pos.ofToSlice_inj {s : String} {p q : s.toSlice.Pos} : ofToSlice p = ofToSlice q ↔ p = q := ⟨fun h => by simpa using congrArg Pos.toSlice h, (· ▸ rfl)⟩ @[simp] @@ -1265,18 +1265,18 @@ theorem Pos.toSlice_le {s : String} {p q : s.Pos} : p.toSlice ≤ q.toSlice ↔ simp [le_iff, Slice.Pos.le_iff] @[simp] -theorem Slice.Pos.ofSlice_le {s : String} {p q : s.toSlice.Pos} : - p.ofSlice ≤ q.ofSlice ↔ p ≤ q := by - simp [String.Pos.le_iff, le_iff] +theorem Pos.ofToSlice_le {s : String} {p q : s.toSlice.Pos} : + ofToSlice p ≤ ofToSlice q ↔ p ≤ q := by + simp [le_iff, Slice.Pos.le_iff] @[simp] theorem Pos.toSlice_lt {s : String} {p q : s.Pos} : p.toSlice < q.toSlice ↔ p < q := by simp [lt_iff, Slice.Pos.lt_iff] @[simp] -theorem Slice.Pos.ofSlice_lt {s : String} {p q : s.toSlice.Pos} : - p.ofSlice < q.ofSlice ↔ p < q := by - simp [String.Pos.lt_iff, lt_iff] +theorem Pos.ofToSlice_lt {s : String} {p q : s.toSlice.Pos} : + ofToSlice p < ofToSlice q ↔ p < q := by + simp [lt_iff, Slice.Pos.lt_iff] /-- Returns the character at the position `pos` of a string, taking a proof that `p` is not the @@ -1290,7 +1290,7 @@ Examples: -/ @[inline, expose] def Pos.get {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : Char := - pos.toSlice.get (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h])) + pos.toSlice.get (ne_of_apply_ne Pos.ofToSlice (by simp [h])) /-- Returns the character at the position `pos` of a string, or `none` if the position is the @@ -1317,7 +1317,7 @@ Returns the byte at the position `pos` of a string. -/ @[inline, expose] def Pos.byte {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : UInt8 := - pos.toSlice.byte (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h])) + pos.toSlice.byte (ne_of_apply_ne Pos.ofToSlice (by simp [h])) theorem Pos.isUTF8FirstByte_byte {s : String} {pos : s.Pos} {h : pos ≠ s.endPos} : (pos.byte h).IsUTF8FirstByte := @@ -1661,60 +1661,56 @@ def Slice.pos! (s : Slice) (off : String.Pos.Raw) : s.Pos := position is not the past-the-end position, which guarantees that such a position exists. -/ @[expose, extern "lean_string_utf8_next_fast"] def Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos := - (Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa))).ofSlice + ofToSlice (Slice.Pos.next pos.toSlice (ne_of_apply_ne Pos.ofToSlice (by simpa))) @[simp] theorem Slice.Pos.str_inj {s : Slice} (p₁ p₂ : s.Pos) : p₁.str = p₂.str ↔ p₁ = p₂ := by simp [Slice.Pos.ext_iff, String.Pos.ext_iff, Pos.Raw.ext_iff] -@[expose, extern "lean_string_utf8_next_fast"] -def String.Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos := - (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] def Pos.next? {s : String} (pos : s.Pos) : Option s.Pos := - pos.toSlice.next?.map Slice.Pos.ofSlice + pos.toSlice.next?.map Pos.ofToSlice /-- Advances a valid position on a string to the next valid position, or panics if the given position is the past-the-end position. -/ @[inline, expose] def Pos.next! {s : String} (pos : s.Pos) : s.Pos := - pos.toSlice.next!.ofSlice + ofToSlice pos.toSlice.next! /-- Returns the previous valid position before the given position, given a proof that the position is not the start position, which guarantees that such a position exists. -/ @[inline, expose] def Pos.prev {s : String} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos := - (pos.toSlice.prev (ne_of_apply_ne Slice.Pos.ofSlice (by simpa))).ofSlice + ofToSlice (pos.toSlice.prev (ne_of_apply_ne Pos.ofToSlice (by simpa))) /-- Returns the previous valid position before the given position, or `none` if the position is the start position. -/ @[inline, expose] def Pos.prev? {s : String} (pos : s.Pos) : Option s.Pos := - pos.toSlice.prev?.map Slice.Pos.ofSlice + pos.toSlice.prev?.map Pos.ofToSlice /-- Returns the previous valid position before the given position, or panics if the position is the start position. -/ @[inline, expose] def Pos.prev! {s : String} (pos : s.Pos) : s.Pos := - pos.toSlice.prev!.ofSlice + ofToSlice pos.toSlice.prev! /-- Constructs a valid position on `s` from a position and a proof that it is valid. -/ @[inline, expose] def pos (s : String) (off : Pos.Raw) (h : off.IsValid s) : s.Pos := - (s.toSlice.pos off h.toSlice).ofSlice + Pos.ofToSlice (s.toSlice.pos off h.toSlice) /-- Constructs a valid position on `s` from a position, returning `none` if the position is not valid. -/ @[inline, expose] def pos? (s : String) (off : Pos.Raw) : Option s.Pos := - (s.toSlice.pos? off).map Slice.Pos.ofSlice + (s.toSlice.pos? off).map Pos.ofToSlice /-- Constructs a valid position `s` from a position, panicking if the position is not valid. -/ @[inline, expose] def pos! (s : String) (off : Pos.Raw) : s.Pos := - (s.toSlice.pos! off).ofSlice + Pos.ofToSlice (s.toSlice.pos! off) @[simp] theorem offset_pos {s : String} {off : Pos.Raw} {h} : (s.pos off h).offset = off := rfl @@ -1814,10 +1810,10 @@ theorem Slice.Pos.prev_ne_endPos {s : Slice} {p : s.Pos} {h} : p.prev h ≠ s.en @[simp] theorem Pos.prev_ne_endPos {s : String} {p : s.Pos} {h} : p.prev h ≠ s.endPos := - mt (congrArg (·.toSlice)) (Slice.Pos.prev_ne_endPos (h := mt (congrArg (·.ofSlice)) h)) + mt (congrArg (·.toSlice)) (Slice.Pos.prev_ne_endPos (h := mt (congrArg Pos.ofToSlice) (by simpa))) theorem Pos.toSlice_prev {s : String} {p : s.Pos} {h} : - (p.prev h).toSlice = p.toSlice.prev (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)) := by + (p.prev h).toSlice = p.toSlice.prev (ne_of_apply_ne Pos.ofToSlice (by simpa)) := by simp [prev] theorem Slice.Pos.offset_prev_lt_offset {s : Slice} {p : s.Pos} {h} : (p.prev h).offset < p.offset := by @@ -1936,7 +1932,7 @@ theorem Pos.get_toSlice {s : String} {p : s.Pos} {h} : rfl theorem Pos.get_eq_get_toSlice {s : String} {p : s.Pos} {h} : - p.get h = p.toSlice.get (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h])) := rfl + p.get h = p.toSlice.get (ne_of_apply_ne Pos.ofToSlice (by simp [h])) := rfl @[simp] theorem Pos.offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) : @@ -1948,7 +1944,7 @@ theorem Pos.byteIdx_offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) : simp theorem Pos.toSlice_next {s : String} {p : s.Pos} {h} : - (p.next h).toSlice = p.toSlice.next (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)) := by + (p.next h).toSlice = p.toSlice.next (ne_of_apply_ne Pos.ofToSlice (by simpa)) := by simp [next] theorem Pos.byteIdx_lt_utf8ByteSize {s : String} (p : s.Pos) (h : p ≠ s.endPos) : @@ -2052,15 +2048,15 @@ theorem Slice.Pos.next_le_of_lt {s : Slice} {p q : s.Pos} {h} : p < q → p.next · have := (p.next h).str.isValid.le_utf8ByteSize simpa [Nat.add_assoc] using this -theorem Slice.Pos.ofSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} : - p.ofSlice ≤ q ↔ p ≤ q.toSlice := Iff.rfl +theorem Pos.ofToSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} : + ofToSlice p ≤ q ↔ p ≤ q.toSlice := Iff.rfl @[simp] theorem Pos.toSlice_lt_toSlice_iff {s : String} {p q : s.Pos} : p.toSlice < q.toSlice ↔ p < q := Iff.rfl theorem Pos.next_le_of_lt {s : String} {p q : s.Pos} {h} : p < q → p.next h ≤ q := by - rw [next, Slice.Pos.ofSlice_le_iff, ← Pos.toSlice_lt_toSlice_iff] + rw [next, Pos.ofToSlice_le_iff, ← Pos.toSlice_lt_toSlice_iff] exact Slice.Pos.next_le_of_lt theorem Slice.Pos.get_eq_get_str {s : Slice} {p : s.Pos} {h} : @@ -2159,11 +2155,8 @@ This happens to be equivalent to the constructor of `String.Slice`. -/ @[inline, expose] -- For the defeq `(s.slice p₁ p₂).str = s` def slice (s : String) (startInclusive endExclusive : s.Pos) - (h : startInclusive ≤ endExclusive) : String.Slice where - str := s - startInclusive - endExclusive - startInclusive_le_endExclusive := h + (h : startInclusive ≤ endExclusive) : String.Slice := + s.toSlice.slice startInclusive.toSlice endExclusive.toSlice (by simpa) @[simp] theorem str_slice {s : String} {startInclusive endExclusive h} : @@ -2171,11 +2164,13 @@ theorem str_slice {s : String} {startInclusive endExclusive h} : @[simp] theorem startInclusive_slice {s : String} {startInclusive endExclusive h} : - (s.slice startInclusive endExclusive h).startInclusive = startInclusive := rfl + (s.slice startInclusive endExclusive h).startInclusive = startInclusive := by + simp [slice] @[simp] theorem endExclusive_slice {s : String} {startInclusive endExclusive h} : - (s.slice startInclusive endExclusive h).endExclusive = endExclusive := rfl + (s.slice startInclusive endExclusive h).endExclusive = endExclusive := by + simp [slice] /-- Given a string and two valid positions within the string, obtain a slice on the string formed by the new bounds, or return `none` if the given end is strictly less then the given start. -/ @@ -2311,6 +2306,127 @@ def Pos.toReplaceEnd {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : pos ≤ p₀ theorem Pos.offset_sliceTo {s : String} {p₀ : s.Pos} {pos : s.Pos} {h : pos ≤ p₀} : (sliceTo p₀ pos h).offset = pos.offset := (rfl) +theorem Pos.Raw.isValidForSlice_slice {s : Slice} {p₀ p₁ : s.Pos} {h} (pos : Pos.Raw) : + pos.IsValidForSlice (s.slice p₀ p₁ h) ↔ + pos.offsetBy p₀.offset ≤ p₁.offset ∧ (pos.offsetBy p₀.offset).IsValidForSlice s := by + refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun ⟨h₁, h₂⟩ => ⟨?_, ?_⟩⟩ + · have : pos.offsetBy p₀.offset ≤ p₁.offset := by + simp [Slice.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at h h₁ ⊢ + omega + exact ⟨this, ⟨Pos.Raw.le_trans this p₁.isValidForSlice.le_rawEndPos, by simpa [offsetBy_assoc]⟩⟩ + · simp [Slice.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at h h₁ ⊢ + omega + · simpa [offsetBy_assoc] using h₂.isValid_offsetBy + +theorem Pos.Raw.isValidForSlice_stringSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : Pos.Raw) : + pos.IsValidForSlice (s.slice p₀ p₁ h) ↔ + pos.offsetBy p₀.offset ≤ p₁.offset ∧ (pos.offsetBy p₀.offset).IsValid s := by + simp [slice, isValidForSlice_slice] + +/-- Given a position in `s.slice p₀ p₁ h`, obtain the corresponding position in `s`. -/ +@[inline] +def Slice.Pos.ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos where + offset := pos.offset.offsetBy p₀.offset + isValidForSlice := (Pos.Raw.isValidForSlice_slice _).1 pos.isValidForSlice |>.2 +@[simp] +theorem Slice.Pos.offset_ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h} {pos : (s.slice p₀ p₁ h).Pos} : + (Pos.ofSlice pos).offset = pos.offset.offsetBy p₀.offset := (rfl) + +/-- Given a position in `s.slice p₀ p₁ h`, obtain the corresponding position in `s`. -/ +@[inline] +def Pos.ofSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos := + ofToSlice (Slice.Pos.ofSlice pos) + +@[simp] +theorem Pos.offset_ofSlice {s : String} {p₀ p₁ : s.Pos} {h} {pos : (s.slice p₀ p₁ h).Pos} : + (Pos.ofSlice pos).offset = pos.offset.offsetBy p₀.offset := (rfl) + +theorem Slice.Pos.le_trans {s : Slice} {p q r : s.Pos} : p ≤ q → q ≤ r → p ≤ r := by + simpa [Pos.le_iff, Pos.Raw.le_iff] using Nat.le_trans + +/-- Given a position in `s` that is between `p₀` and `p₁`, obtain the corresponding position in +`s.slice p₀ p₁ h`. -/ +@[inline] +def Slice.Pos.slice {s : Slice} (pos : s.Pos) (p₀ p₁ : s.Pos) (h₁ : p₀ ≤ pos) (h₂ : pos ≤ p₁) : + (s.slice p₀ p₁ (Slice.Pos.le_trans h₁ h₂)).Pos where + offset := pos.offset.unoffsetBy p₀.offset + isValidForSlice := (Pos.Raw.isValidForSlice_slice _).2 + (by simp [Pos.Raw.offsetBy_unoffsetBy_of_le h₁, Slice.Pos.le_iff.1 h₂, pos.isValidForSlice]) + +/-- Given a position in `s` that is between `p₀` and `p₁`, obtain the corresponding position in +`s.slice p₀ p₁ h`. -/ +@[inline] +def Pos.slice {s : String} (pos : s.Pos) (p₀ p₁ : s.Pos) (h₁ : p₀ ≤ pos) (h₂ : pos ≤ p₁) : + (s.slice p₀ p₁ (Pos.le_trans h₁ h₂)).Pos := + Slice.Pos.slice pos.toSlice _ _ h₁ h₂ + +@[simp] +theorem Pos.offset_slice {s : String} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁} : + (pos.slice p₀ p₁ h₁ h₂).offset = pos.offset.unoffsetBy p₀.offset := (rfl) + +/-- +Given a position in `s`, obtain the corresponding position in `s.slice p₀ p₁ h`, or panic if `pos` +is not between `p₀` and `p₁`. +-/ +@[inline] +def Slice.Pos.sliceOrPanic {s : Slice} (pos : s.Pos) (p₀ p₁ : s.Pos) {h} : + (s.slice p₀ p₁ h).Pos := + if h : p₀ ≤ pos ∧ pos ≤ p₁ then + pos.slice p₀ p₁ h.1 h.2 + else + panic! "Position is outside of the bounds of the slice." + +/-- +Given a position in `s`, obtain the corresponding position in `s.slice p₀ p₁ h`, or panic if `pos` +is not between `p₀` and `p₁`. +-/ +@[inline] +def Pos.sliceOrPanic {s : String} (pos : s.Pos) (p₀ p₁ : s.Pos) {h} : + (s.slice p₀ p₁ h).Pos := + Slice.Pos.sliceOrPanic pos.toSlice _ _ + +theorem Slice.slice_eq_slice! {s : Slice} {p₀ p₁ h} : s.slice p₀ p₁ h = s.slice! p₀ p₁ := by + simp [slice!, h] + +theorem slice_eq_slice! {s : String} {p₀ p₁ h} : s.slice p₀ p₁ h = s.slice! p₀ p₁ := by + simp [slice!, slice, Slice.slice_eq_slice!] + +/-- Given a position in `s.slice! p₀ p₁`, obtain the corresponding position in `s`, or panic if +taking `s.slice! p₀ p₁` already panicked. -/ +@[inline] +def Slice.Pos.ofSlice! {s : Slice} {p₀ p₁ : s.Pos} (pos : (s.slice! p₀ p₁).Pos) : s.Pos := + if h : p₀ ≤ p₁ then + ofSlice (h := h) (pos.cast slice_eq_slice!.symm) + else + panic! "Starting position must be less than or equal to end position." + +/-- Given a position in `s.slice! p₀ p₁`, obtain the corresponding position in `s`, or panic if +taking `s.slice! p₀ p₁` already panicked. -/ +@[inline] +def Pos.ofSlice! {s : String} {p₀ p₁ : s.Pos} (pos : (s.slice! p₀ p₁).Pos) : s.Pos := + ofToSlice (Slice.Pos.ofSlice! pos) + +/-- +Given a position in `s`, obtain the corresponding position in `s.slice! p₀ p₁ h`, or panic if +taking `s.slice! p₀ p₁` already panicked or if the position is not between `p₀` and `p₁`. +-/ +@[inline] +def Slice.Pos.slice! {s : Slice} (pos : s.Pos) (p₀ p₁ : s.Pos) : + (s.slice! p₀ p₁).Pos := + if h : p₀ ≤ pos ∧ pos ≤ p₁ then + (pos.slice _ _ h.1 h.2).cast slice_eq_slice! + else + panic! "Starting position must be less than or equal to end position and position must be between starting position and end position." + +/-- +Given a position in `s`, obtain the corresponding position in `s.slice! p₀ p₁ h`, or panic if +taking `s.slice! p₀ p₁` already panicked or if the position is not between `p₀` and `p₁`. +-/ +@[inline] +def Pos.slice! {s : String} (pos : s.Pos) (p₀ p₁ : s.Pos) : + (s.slice! p₀ p₁).Pos := + Slice.Pos.slice! pos.toSlice _ _ + /-- Advances the position `p` `n` times. @@ -2346,7 +2462,7 @@ If this would move `p` past the end of `s`, the result is `s.endPos`. -/ @[inline] def Pos.nextn {s : String} (p : s.Pos) (n : Nat) : s.Pos := - (p.toSlice.nextn n).ofSlice + ofToSlice (p.toSlice.nextn n) /-- Iterates `p.prev` `n` times. @@ -2355,7 +2471,7 @@ If this would move `p` past the start of `s`, the result is `s.startPos`. -/ @[inline] def Pos.prevn {s : String} (p : s.Pos) (n : Nat) : s.Pos := - (p.toSlice.prevn n).ofSlice + ofToSlice (p.toSlice.prevn n) theorem Slice.Pos.le_nextn {s : Slice} {p : s.Pos} {n : Nat} : p ≤ p.nextn n := by fun_induction nextn with diff --git a/src/Init/Data/String/Search.lean b/src/Init/Data/String/Search.lean index 059ae87369..258710d585 100644 --- a/src/Init/Data/String/Search.lean +++ b/src/Init/Data/String/Search.lean @@ -94,7 +94,7 @@ Examples: @[inline] def Pos.find? {s : String} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher pattern σ] : Option s.Pos := - (pos.toSlice.find? pattern).map (·.ofSlice) + (pos.toSlice.find? pattern).map Pos.ofToSlice /-- Finds the position of the first match of the pattern {name}`pattern` in after the position @@ -109,7 +109,7 @@ Examples: @[inline] def Pos.find {s : String} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher pattern σ] : s.Pos := - (pos.toSlice.find pattern).ofSlice + ofToSlice (pos.toSlice.find pattern) /-- Finds the position of the first match of the pattern {name}`pattern` in a string {name}`s`. If @@ -172,7 +172,7 @@ Examples: @[inline] def Pos.revFind? {s : String} (pos : s.Pos) (pattern : ρ) [ToBackwardSearcher pattern σ] : Option s.Pos := - (pos.toSlice.revFind? pattern).map (·.ofSlice) + (pos.toSlice.revFind? pattern).map Pos.ofToSlice /-- Finds the position of the first match of the pattern {name}`pattern` in a string, starting @@ -539,14 +539,14 @@ Examples: @[inline, expose] def back (s : String) : Char := s.toSlice.back -theorem Slice.Pos.ofSlice_ne_endPos {s : String} {p : s.toSlice.Pos} - (h : p ≠ s.toSlice.endPos) : p.ofSlice ≠ s.endPos := by - rwa [ne_eq, ← Pos.toSlice_inj, toSlice_ofSlice, ← endPos_toSlice] +theorem Pos.ofToSlice_ne_endPos {s : String} {p : s.toSlice.Pos} + (h : p ≠ s.toSlice.endPos) : ofToSlice p ≠ s.endPos := by + rwa [ne_eq, ← Pos.toSlice_inj, Slice.Pos.toSlice_ofToSlice, ← endPos_toSlice] @[inline] def Internal.toSliceWithProof {s : String} : { p : s.toSlice.Pos // p ≠ s.toSlice.endPos } → { p : s.Pos // p ≠ s.endPos } := - fun ⟨p, h⟩ => ⟨p.ofSlice, Slice.Pos.ofSlice_ne_endPos h⟩ + fun ⟨p, h⟩ => ⟨Pos.ofToSlice p, Pos.ofToSlice_ne_endPos h⟩ /-- Creates an iterator over all valid positions within {name}`s`.