theorem String.Slice.skipPrefix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : s.skipPrefix? pat = some s.startPos

@[simp]

theorem String.Slice.skipPrefix?_slice_eq_some_iff {pat s : Slice} {pos : s.Pos} : s.skipPrefix? pat = some pos ↔ ∃ (t : String), pos.Splits pat.copy t

theorem String.Slice.startsWith_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : s.startsWith pat = true

@[simp]

theorem String.Slice.startsWith_slice_iff {pat s : Slice} : s.startsWith pat = true ↔ pat.copy.toList <+: s.copy.toList

@[simp]

theorem String.Slice.startsWith_slice_eq_false_iff {pat s : Slice} : s.startsWith pat = false ↔ ¬pat.copy.toList <+: s.copy.toList

theorem String.Slice.dropPrefix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : s.dropPrefix? pat = some s

theorem String.Slice.eq_append_of_dropPrefix?_slice_eq_some {pat s res : Slice} (h : s.dropPrefix? pat = some res) : s.copy = pat.copy ++ res.copy

@[simp]

theorem String.Slice.skipPrefix?_string_eq_some_iff {pat : String} {s : Slice} {pos : s.Pos} : s.skipPrefix? pat = some pos ↔ ∃ (t : String), pos.Splits pat t

@[simp]

theorem String.Slice.skipPrefix?_string_empty {s : Slice} : s.skipPrefix? "" = some s.startPos

@[simp]

theorem String.Slice.startsWith_string_iff {pat : String} {s : Slice} : s.startsWith pat = true ↔ pat.toList <+: s.copy.toList

@[simp]

theorem String.Slice.startsWith_string_empty {s : Slice} : s.startsWith "" = true

@[simp]

theorem String.Slice.startsWith_string_eq_false_iff {pat : String} {s : Slice} : s.startsWith pat = false ↔ ¬pat.toList <+: s.copy.toList

@[simp]

theorem String.Slice.dropPrefix?_string_empty {s : Slice} : s.dropPrefix? "" = some s

theorem String.Slice.eq_append_of_dropPrefix?_string_eq_some {pat : String} {s res : Slice} (h : s.dropPrefix? pat = some res) : s.copy = pat ++ res.copy

theorem String.Slice.skipSuffix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : s.skipSuffix? pat = some s.endPos

@[simp]

theorem String.Slice.skipSuffix?_slice_eq_some_iff {pat s : Slice} {pos : s.Pos} : s.skipSuffix? pat = some pos ↔ ∃ (t : String), pos.Splits t pat.copy

theorem String.Slice.endsWith_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : s.endsWith pat = true

@[simp]

theorem String.Slice.endsWith_slice_iff {pat s : Slice} : s.endsWith pat = true ↔ pat.copy.toList <:+ s.copy.toList

@[simp]

theorem String.Slice.endsWith_slice_eq_false_iff {pat s : Slice} : s.endsWith pat = false ↔ ¬pat.copy.toList <:+ s.copy.toList

theorem String.Slice.dropSuffix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) : s.dropSuffix? pat = some s

theorem String.Slice.eq_append_of_dropSuffix?_slice_eq_some {pat s res : Slice} (h : s.dropSuffix? pat = some res) : s.copy = res.copy ++ pat.copy

@[simp]

theorem String.Slice.skipSuffix?_string_eq_some_iff' {pat : String} {s : Slice} {pos : s.Pos} : s.skipSuffix? pat = some pos ↔ ∃ (t : String), pos.Splits t pat

@[simp]

theorem String.Slice.skipSuffix?_string_empty {s : Slice} : s.skipSuffix? "" = some s.endPos

@[simp]

theorem String.Slice.endsWith_string_iff {pat : String} {s : Slice} : s.endsWith pat = true ↔ pat.toList <:+ s.copy.toList

@[simp]

theorem String.Slice.endsWith_string_empty {s : Slice} : s.endsWith "" = true

@[simp]

theorem String.Slice.endsWith_string_eq_false_iff {pat : String} {s : Slice} : s.endsWith pat = false ↔ ¬pat.toList <:+ s.copy.toList

@[simp]

theorem String.Slice.dropSuffix?_string_empty {s : Slice} : s.dropSuffix? "" = some s

theorem String.Slice.eq_append_of_dropSuffix?_string_eq_some {pat : String} {s res : Slice} (h : s.dropSuffix? pat = some res) : s.copy = res.copy ++ pat

theorem String.skipPrefix?_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) : s.skipPrefix? pat = some s.startPos

@[simp]

theorem String.skipPrefix?_slice_eq_some_iff {pat : Slice} {s : String} {pos : s.Pos} : s.skipPrefix? pat = some pos ↔ ∃ (t : String), pos.Splits pat.copy t

theorem String.startsWith_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) : s.startsWith pat = true

@[simp]

theorem String.startsWith_slice_iff {pat : Slice} {s : String} : s.startsWith pat = true ↔ pat.copy.toList <+: s.toList

@[simp]

theorem String.startsWith_slice_eq_false_iff {pat : Slice} {s : String} : s.startsWith pat = false ↔ ¬pat.copy.toList <+: s.toList

theorem String.dropPrefix?_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) : s.dropPrefix? pat = some s.toSlice

theorem String.eq_append_of_dropPrefix?_slice_eq_some {pat res : Slice} {s : String} (h : s.dropPrefix? pat = some res) : s = pat.copy ++ res.copy

@[simp]

theorem String.skipPrefix?_string_empty {s : String} : s.skipPrefix? "" = some s.startPos

@[simp]

theorem String.skipPrefix?_string_eq_some_iff {pat s : String} {pos : s.Pos} : s.skipPrefix? pat = some pos ↔ ∃ (t : String), pos.Splits pat t

@[simp]

theorem String.startsWith_string_empty {s : String} : s.startsWith "" = true

@[simp]

theorem String.startsWith_string_iff {pat s : String} : s.startsWith pat = true ↔ pat.toList <+: s.toList

@[simp]

theorem String.startsWith_string_eq_false_iff {pat s : String} : s.startsWith pat = false ↔ ¬pat.toList <+: s.toList

@[simp]

theorem String.dropPrefix?_string_empty {s : String} : s.dropPrefix? "" = some s.toSlice

theorem String.eq_append_of_dropPrefix?_string_eq_some {s pat : String} {res : Slice} (h : s.dropPrefix? pat = some res) : s = pat ++ res.copy