def String.Slice.isSubslice (s t : Slice) : Prop

Slice s is a subslice of Slice t, if the underlying strings are equal and t.startInclusive ≤ s.startInclusive and s.endExclusive ≤ t.endExclusive.

Equations

• s.isSubslice t = (s.str = t.str ∧ t.startInclusive.offset ≤ s.startInclusive.offset ∧ s.endExclusive.offset ≤ t.endExclusive.offset)

@[simp]

theorem String.Slice.replaceStartEnd_is_subslice_of {s : Slice} {p0 p1 : s.Pos} {h : p0 ≤ p1} : (s.replaceStartEnd p0 p1 h).isSubslice s

def String.Slice.castPosOfSubslice {s t : Slice} (p : s.Pos) (h : s.isSubslice t) : t.Pos

cast p : s.Pos to t.Pos

Equations

• String.Slice.castPosOfSubslice p h = { offset := { byteIdx := p.offset.byteIdx + s.startInclusive.offset.byteIdx - t.startInclusive.offset.byteIdx }, isValidForSlice := ⋯ }

def String.Slice.startPosOfSubslice {s t : Slice} (h : s.isSubslice t) : t.Pos

s.startPos : s.Pos as t.Pos

Equations

• String.Slice.startPosOfSubslice h = String.Slice.castPosOfSubslice s.startPos h

theorem String.Slice.startPosOfSubslice_eq {s t : Slice} (h : s.isSubslice t) : { byteIdx := s.startInclusive.offset.byteIdx - t.startInclusive.offset.byteIdx } = (startPosOfSubslice h).offset

def String.Slice.endPosOfSubslice {s t : Slice} (h : s.isSubslice t) : t.Pos

s.endPos : s.Pos as t.Pos

Equations

• String.Slice.endPosOfSubslice h = String.Slice.castPosOfSubslice s.endPos h

theorem String.Slice.endPosOfSubslice_eq {s t : Slice} (h : s.isSubslice t) : { byteIdx := s.endExclusive.offset.byteIdx - t.startInclusive.offset.byteIdx } = (endPosOfSubslice h).offset

@[simp]

theorem String.Slice.byteDistance_of_next_lt {s : Slice} {pos : s.Pos} (h : pos ≠ s.endPos) : (pos.next h).offset.byteDistance s.rawEndPos < pos.offset.byteDistance s.rawEndPos

@[simp]

theorem String.Slice.byteDistance_of_offset_and_char_lt {s : Slice} {pos : s.Pos} (h : pos ≠ s.endPos) : (pos.offset + pos.get h).byteDistance s.rawEndPos < pos.offset.byteDistance s.rawEndPos