structure String.Slice.Subslice (s : Slice) : Type

A region or slice of a fixed slice.

Given a Slice s, the type s.Subslice is the type of half-open regions in s delineated by a valid position on both sides.

This type is useful to track regions of interest within some larger slice that is also of interest. In contrast, Slice is used to track regions of interest whithin some larger string that is not or no longer relevant.

Equality on Subslice is somewhat better behaved than on Slice, but note that there will in general be many different representations of the empty subslice of a slice.

• startInclusive : s.Pos

  The byte position of the start of the subslice.

• endExclusive : s.Pos

  The byte position of the end of the subslice.

• startInclusive_le_endExclusive : self.startInclusive ≤ self.endExclusive

  The subslice is not degenerate (but it may be empty).

theorem String.Slice.Subslice.ext {s : Slice} {x y : s.Subslice} (startInclusive : x.startInclusive = y.startInclusive) (endExclusive : x.endExclusive = y.endExclusive) : x = y

theorem String.Slice.Subslice.ext_iff {s : Slice} {x y : s.Subslice} : x = y ↔ x.startInclusive = y.startInclusive ∧ x.endExclusive = y.endExclusive

@[implicit_reducible]

instance String.Slice.instInhabitedSubslice {s : Slice} : Inhabited s.Subslice

@[inline]

def String.Slice.Subslice.toSlice {s : Slice} (sl : s.Subslice) : Slice

Turns a subslice into a standalone slice by "forgetting" which slice the subslice is a sublice of.

@[simp]

theorem String.Slice.Subslice.str_toSlice {s : Slice} {sl : s.Subslice} : sl.toSlice.str = s.str

@[simp]

theorem String.Slice.Subslice.startInclusive_toSlice {s : Slice} {sl : s.Subslice} : sl.toSlice.startInclusive = sl.startInclusive.str

@[simp]

theorem String.Slice.Subslice.endExclusive_toSlice {s : Slice} {sl : s.Subslice} : sl.toSlice.endExclusive = sl.endExclusive.str

@[implicit_reducible]

instance String.Slice.Subslice.instCoeOut {s : Slice} : CoeOut s.Subslice Slice

@[inline]

def String.Slice.Subslice.copy {s : Slice} (sl : s.Subslice) : String

Creates a String from a Subslice by copying out the bytes.

@[inline]

def String.Slice.Subslice.toString {s : Slice} (sl : s.Subslice) : String

Creates a String from a Subslice by copying out the bytes.

@[implicit_reducible]

instance String.Slice.Subslice.instToString {s : Slice} : ToString s.Subslice

@[inline]

def String.Slice.subslice (s : Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd) : s.Subslice

Constructs a subslice of s given the bounds of the subslice and a proof that the subslice is non-degenerate.

@[simp]

theorem String.Slice.toSlice_subslice {s : Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd} : (s.subslice newStart newEnd h).toSlice = s.slice newStart newEnd h

@[simp]

theorem String.Slice.startInclusive_subslice {s : Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd} : (s.subslice newStart newEnd h).startInclusive = newStart

@[simp]

theorem String.Slice.endExclusive_subslice {s : Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd} : (s.subslice newStart newEnd h).endExclusive = newEnd

def String.Slice.subslice! (s : Slice) (newStart newEnd : s.Pos) : s.Subslice

Constructs a subslice of s given the bounds of the subslice. If the subslice would be degenerate, this function panics.

theorem String.Slice.subslice!_eq_subslice {s : Slice} {newStart newEnd : s.Pos} (h : newStart ≤ newEnd) : s.subslice! newStart newEnd = s.subslice newStart newEnd h

@[inline]

def String.Slice.subsliceFrom (s : Slice) (newStart : s.Pos) : s.Subslice

Constructs a subslice of s starting at the given position and going until the end of the slice.

@[simp]

theorem String.Slice.startInclusive_subsliceFrom {s : Slice} {newStart : s.Pos} : (s.subsliceFrom newStart).startInclusive = newStart

@[simp]

theorem String.Slice.endExclusive_subsliceFrom {s : Slice} {newStart : s.Pos} : (s.subsliceFrom newStart).endExclusive = s.endPos

@[inline]

def String.Slice.toSubslice (s : Slice) : s.Subslice

The entire slice, as a subslice of itself.

@[simp]

theorem String.Slice.startInclusive_toSubslice {s : Slice} : s.toSubslice.startInclusive = s.startPos

@[simp]

theorem String.Slice.endExclusive_toSubslice {s : Slice} : s.toSubslice.endExclusive = s.endPos

@[inline]

def String.Slice.Subslice.ofSliceFrom {s : Slice} {p : s.Pos} (sl : (s.sliceFrom p).Subslice) : s.Subslice

Given a position p within a slice s and a subslice sl of s.sliceFrom p, reinterpret sl as a subslice of s by applying Pos.ofSliceFrom to the endpoints.

@[simp]

theorem String.Slice.Subslice.startInclusive_ofSliceFrom {s : Slice} {p : s.Pos} {sl : (s.sliceFrom p).Subslice} : sl.ofSliceFrom.startInclusive = Pos.ofSliceFrom sl.startInclusive

@[simp]

theorem String.Slice.Subslice.endExclusive_ofSliceFrom {s : Slice} {p : s.Pos} {sl : (s.sliceFrom p).Subslice} : sl.ofSliceFrom.endExclusive = Pos.ofSliceFrom sl.endExclusive

@[inline]

def String.Slice.Subslice.extendLeft {s : Slice} (sl : s.Subslice) (newStart : s.Pos) (h : newStart ≤ sl.startInclusive) : s.Subslice

Given a subslice sl of s and a position newStart that is at most the start position of the subslice, obtain a new subslice whose start is newStart and whose end is the end of sl.

@[simp]

theorem String.Slice.Subslice.startInclusive_extendLeft {s : Slice} {sl : s.Subslice} {newStart : s.Pos} {h : newStart ≤ sl.startInclusive} : (sl.extendLeft newStart h).startInclusive = newStart

@[simp]

theorem String.Slice.Subslice.endExclusive_extendLeft {s : Slice} {sl : s.Subslice} {newStart : s.Pos} {h : newStart ≤ sl.startInclusive} : (sl.extendLeft newStart h).endExclusive = sl.endExclusive

@[simp]

theorem String.Slice.Subslice.extendLeft_extendLeft {s : Slice} {sl : s.Subslice} (p₁ p₂ : s.Pos) (h₂ : p₂ ≤ sl.startInclusive) (h₁ : p₁ ≤ (sl.extendLeft p₂ h₂).startInclusive) : (sl.extendLeft p₂ h₂).extendLeft p₁ h₁ = sl.extendLeft p₁ ⋯

@[simp]

theorem String.Slice.Subslice.extendLeft_self {s : Slice} {sl : s.Subslice} : sl.extendLeft sl.startInclusive ⋯ = sl

@[inline]

def String.Slice.Subslice.cast {s t : Slice} (h : s = t) (sl : s.Subslice) : t.Subslice

Given a subslice of s and a proof that s = t, obtain the corresponding subslice of t.

@[simp]

theorem String.Slice.Subslice.startInclusive_cast {s t : Slice} {h : s = t} {sl : s.Subslice} : (cast h sl).startInclusive = sl.startInclusive.cast h

@[simp]

theorem String.Slice.Subslice.endExclusive_cast {s t : Slice} {h : s = t} {sl : s.Subslice} : (cast h sl).endExclusive = sl.endExclusive.cast h

@[simp]

theorem String.Slice.Subslice.cast_rfl {s : Slice} : cast ⋯ = id