theorem String.Slice.drop_eq_sliceFrom {s : Slice} {n : Nat} : s.drop n = s.sliceFrom (s.startPos.nextn n)

@[simp]

theorem String.Slice.toList_copy_drop {s : Slice} {n : Nat} : (s.drop n).copy.toList = List.drop n s.copy.toList

theorem String.Slice.dropEnd_eq_sliceTo {s : Slice} {n : Nat} : s.dropEnd n = s.sliceTo (s.endPos.prevn n)

@[simp]

theorem String.Slice.toList_copy_dropEnd {s : Slice} {n : Nat} : (s.dropEnd n).copy.toList = List.take (s.copy.length - n) s.copy.toList

theorem String.Slice.take_eq_sliceTo {s : Slice} {n : Nat} : s.take n = s.sliceTo (s.startPos.nextn n)

@[simp]

theorem String.Slice.toList_copy_take {s : Slice} {n : Nat} : (s.take n).copy.toList = List.take n s.copy.toList

theorem String.Slice.takeEnd_eq_sliceFrom {s : Slice} {n : Nat} : s.takeEnd n = s.sliceFrom (s.endPos.prevn n)

@[simp]

theorem String.Slice.toList_copy_takeEnd {s : Slice} {n : Nat} : (s.takeEnd n).copy.toList = List.drop (s.copy.length - n) s.copy.toList

@[simp]

theorem String.drop_toSlice {s : String} {n : Nat} : s.toSlice.drop n = s.drop n

@[simp]

theorem String.toList_copy_drop {s : String} {n : Nat} : (s.drop n).copy.toList = List.drop n s.toList

@[simp]

theorem String.dropEnd_toSlice {s : String} {n : Nat} : s.toSlice.dropEnd n = s.dropEnd n

@[simp]

theorem String.toList_copy_dropEnd {s : String} {n : Nat} : (s.dropEnd n).copy.toList = List.take (s.length - n) s.toList

@[simp]

theorem String.take_toSlice {s : String} {n : Nat} : s.toSlice.take n = s.take n

@[simp]

theorem String.toList_copy_take {s : String} {n : Nat} : (s.take n).copy.toList = List.take n s.toList

@[simp]

theorem String.takeEnd_toSlice {s : String} {n : Nat} : s.toSlice.takeEnd n = s.takeEnd n

@[simp]

theorem String.toList_copy_takeEnd {s : String} {n : Nat} : (s.takeEnd n).copy.toList = List.drop (s.length - n) s.toList