@[simp]

theorem String.Slice.beq_eq_true_iff {s t : Slice} : (s == t) = true ↔ s.copy = t.copy

@[simp]

theorem String.Slice.beq_eq_false_iff {s t : Slice} : (s == t) = false ↔ s.copy ≠ t.copy

theorem String.Slice.beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy)

instance String.Slice.instEquivBEq : EquivBEq Slice

theorem String.Slice.beq_list_iff {l l' : List Slice} : (l == l') = true ↔ List.map copy l = List.map copy l'

theorem String.Slice.beq_list_eq_false_iff {l l' : List Slice} : (l == l') = false ↔ List.map copy l ≠ List.map copy l'

theorem String.Slice.beq_list_eq_decide {l l' : List Slice} : (l == l') = decide (List.map copy l = List.map copy l')

theorem String.Slice.Pos.get?_eq_dif {s : Slice} {p : s.Pos} : p.get? = if h : p = s.endPos then none else some (p.get h)

theorem String.Slice.Pos.get?_eq_some_get {s : Slice} {p : s.Pos} (h : p ≠ s.endPos) : p.get? = some (p.get h)

@[simp]

theorem String.Slice.Pos.get?_eq_none_iff {s : Slice} {p : s.Pos} : p.get? = none ↔ p = s.endPos

theorem String.Slice.Pos.get?_eq_none {s : Slice} {p : s.Pos} (h : p = s.endPos) : p.get? = none

@[simp]

theorem String.Slice.Pos.get?_endPos {s : Slice} : s.endPos.get? = none

theorem String.Pos.get?_toSlice {s : String} {p : s.Pos} : p.toSlice.get? = p.get?

theorem String.Pos.get?_eq_dif {s : String} {p : s.Pos} : p.get? = if h : p = s.endPos then none else some (p.get h)

theorem String.Pos.get?_eq_some_get {s : String} {p : s.Pos} (h : p ≠ s.endPos) : p.get? = some (p.get h)

@[simp]

theorem String.Pos.get?_eq_none_iff {s : String} {p : s.Pos} : p.get? = none ↔ p = s.endPos

theorem String.Pos.get?_eq_none {s : String} {p : s.Pos} (h : p = s.endPos) : p.get? = none

@[simp]

theorem String.Pos.get?_endPos {s : String} : s.endPos.get? = none

theorem String.Slice.front?_eq_get? {s : Slice} : s.front? = s.startPos.get?

theorem String.Slice.front?_eq {s : Slice} : s.front? = s.copy.toList.head?

@[simp]

theorem String.Slice.front_eq {s : Slice} : s.front = s.front?.getD default

theorem String.Slice.back?_eq_get? {s : Slice} : s.back? = s.endPos.prev?.bind Pos.get?

theorem String.Slice.back?_eq {s : Slice} : s.back? = s.copy.toList.getLast?

@[simp]

theorem String.Slice.back_eq {s : Slice} : s.back = s.back?.getD default