Init.Data.Slice.List.Lemmas

instance ListSlice.instLawfulSliceSizeTakeListIteratorIdListSliceData {α : Type u_1} :

Std.Slice.LawfulSliceSize (Std.Slice.Internal.ListSliceData α)

theorem ListSlice.toList_eq {α : Type u_1} {xs : ListSlice α} :

Std.Slice.toList xs = match Std.Slice.Internal.ListSliceData.stop α with | some stop => List.take stop Std.Slice.Internal.ListSliceData.list | none => Std.Slice.Internal.ListSliceData.list

source

theorem ListSlice.toArray_toList {α : Type u_1} {xs : ListSlice α} :

(Std.Slice.toList xs).toArray = Std.Slice.toArray xs

source

theorem ListSlice.toList_toArray {α : Type u_1} {xs : ListSlice α} :

(Std.Slice.toArray xs).toList = Std.Slice.toList xs

source

@[simp]

theorem ListSlice.length_toList {α : Type u_1} {xs : ListSlice α} :

(Std.Slice.toList xs).length = Std.Slice.size xs

source

@[simp]

theorem ListSlice.size_toArray {α : Type u_1} {xs : ListSlice α} :

(Std.Slice.toArray xs).size = Std.Slice.size xs

source

@[simp]

theorem List.toList_mkSlice_rco {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...hi) = drop lo (take hi xs)

source

@[simp]

theorem List.toArray_mkSlice_rco {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...hi) = (drop lo (take hi xs)).toArray

source

@[simp]

theorem List.size_mkSlice_rco {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.size (Std.Rco.Sliceable.mkSlice xs lo...hi) = min hi xs.length - lo

source

@[simp]

theorem List.mkSlice_rcc_eq_mkSlice_rco {α : Type u_1} {xs : List α} {lo hi : Nat} :

(Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1

source

@[simp]

theorem List.toList_mkSlice_rcc {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = drop lo (take (hi + 1) xs)

source

@[simp]

theorem List.toArray_mkSlice_rcc {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = (drop lo (take (hi + 1) xs)).toArray

source

@[simp]

theorem List.size_mkSlice_rcc {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = min (hi + 1) xs.length - lo

source

@[simp]

theorem List.toList_mkSlice_rci {α : Type u_1} {xs : List α} {lo : Nat} :

Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = drop lo xs

source

@[simp]

theorem List.toArray_mkSlice_rci {α : Type u_1} {xs : List α} {lo : Nat} :

Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = (drop lo xs).toArray

source

@[simp]

theorem List.size_mkSlice_rci {α : Type u_1} {xs : List α} {lo : Nat} :

Std.Slice.size (Std.Rci.Sliceable.mkSlice xs lo...*) = xs.length - lo

source

@[simp]

theorem List.mkSlice_roo_eq_mkSlice_rco {α : Type u_1} {xs : List α} {lo hi : Nat} :

(Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi

source

@[simp]

theorem List.toList_mkSlice_roo {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...hi) = drop (lo + 1) (take hi xs)

source

@[simp]

theorem List.toArray_mkSlice_roo {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...hi) = (drop (lo + 1) (take hi xs)).toArray

source

@[simp]

theorem List.size_mkSlice_roo {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.size (Std.Roo.Sliceable.mkSlice xs lo<...hi) = min hi xs.length - (lo + 1)

source

@[simp]

theorem List.mkSlice_roc_eq_mkSlice_roo {α : Type u_1} {xs : List α} {lo hi : Nat} :

(Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1

source

@[simp]

theorem List.toList_mkSlice_roc {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = drop (lo + 1) (take (hi + 1) xs)

source

@[simp]

theorem List.toArray_mkSlice_roc {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = (drop (lo + 1) (take (hi + 1) xs)).toArray

source

@[simp]

theorem List.size_mkSlice_roc {α : Type u_1} {xs : List α} {lo hi : Nat} :

Std.Slice.size (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = min (hi + 1) xs.length - (lo + 1)

source

@[simp]

theorem List.mkSlice_roi_eq_mkSlice_rci {α : Type u_1} {xs : List α} {lo : Nat} :

Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*

source

@[simp]

theorem List.toList_mkSlice_roi {α : Type u_1} {xs : List α} {lo : Nat} :

Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = drop (lo + 1) xs

source

@[simp]

theorem List.toArray_mkSlice_roi {α : Type u_1} {xs : List α} {lo : Nat} :

Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = (drop (lo + 1) xs).toArray

source

@[simp]

theorem List.size_mkSlice_roi {α : Type u_1} {xs : List α} {lo : Nat} :

Std.Slice.size (Std.Roi.Sliceable.mkSlice xs lo<...*) = xs.length - (lo + 1)

source

@[simp]

theorem List.mkSlice_rio_eq_mkSlice_rco {α : Type u_1} {xs : List α} {hi : Nat} :

(Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi

source

@[simp]

theorem List.toList_mkSlice_rio {α : Type u_1} {xs : List α} {hi : Nat} :

Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = take hi xs

source

@[simp]

theorem List.toArray_mkSlice_rio {α : Type u_1} {xs : List α} {hi : Nat} :

Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = (take hi xs).toArray

source

@[simp]

theorem List.size_mkSlice_rio {α : Type u_1} {xs : List α} {hi : Nat} :

Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi xs.length

source

@[simp]

theorem List.mkSlice_ric_eq_mkSlice_rio {α : Type u_1} {xs : List α} {hi : Nat} :

(Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1

source

@[simp]

theorem List.toList_mkSlice_ric {α : Type u_1} {xs : List α} {hi : Nat} :

Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = take (hi + 1) xs

source

@[simp]

theorem List.toArray_mkSlice_ric {α : Type u_1} {xs : List α} {hi : Nat} :

Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = (take (hi + 1) xs).toArray

source

@[simp]

theorem List.size_mkSlice_ric {α : Type u_1} {xs : List α} {hi : Nat} :

Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) xs.length

source

@[simp]

theorem List.mkSlice_rii_eq_mkSlice_rci {α : Type u_1} {xs : List α} :

Std.Rii.Sliceable.mkSlice xs *...* = Std.Rci.Sliceable.mkSlice xs 0...*

source

@[simp]

theorem List.toList_mkSlice_rii {α : Type u_1} {xs : List α} :

Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = xs

source

@[simp]

theorem List.toArray_mkSlice_rii {α : Type u_1} {xs : List α} :

Std.Slice.toArray (Std.Rii.Sliceable.mkSlice xs *...*) = xs.toArray

source

@[simp]

theorem List.size_mkSlice_rii {α : Type u_1} {xs : List α} :

Std.Slice.size (Std.Rii.Sliceable.mkSlice xs *...*) = xs.length

source

@[simp]

theorem ListSlice.toList_mkSlice_rco {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...hi) = List.drop lo (List.take hi (Std.Slice.toList xs))

source

@[simp]

theorem ListSlice.toArray_mkSlice_rco {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...hi) = (Std.Slice.toArray xs).extract lo hi

source

@[simp]

theorem ListSlice.mkSlice_rcc_eq_mkSlice_rco {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

(Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1

source

@[simp]

theorem ListSlice.toList_mkSlice_rcc {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = List.drop lo (List.take (hi + 1) (Std.Slice.toList xs))

source

@[simp]

theorem ListSlice.toArray_mkSlice_rcc {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = (Std.Slice.toArray xs).extract lo (hi + 1)

source

@[simp]

theorem ListSlice.toList_mkSlice_rci {α : Type u_1} {xs : ListSlice α} {lo : Nat} :

Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = List.drop lo (Std.Slice.toList xs)

source

@[simp]

theorem ListSlice.toArray_mkSlice_rci {α : Type u_1} {xs : ListSlice α} {lo : Nat} :

Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = (Std.Slice.toArray xs).extract lo

source

@[simp]

theorem ListSlice.mkSlice_roo_eq_mkSlice_rco {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

(Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi

source

@[simp]

theorem ListSlice.toList_mkSlice_roo {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...hi) = List.drop (lo + 1) (List.take hi (Std.Slice.toList xs))

source

@[simp]

theorem ListSlice.toArray_mkSlice_roo {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...hi) = (Std.Slice.toArray xs).extract (lo + 1) hi

source

@[simp]

theorem ListSlice.mkSlice_roc_eq_mkSlice_roo {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

(Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1

source

@[simp]

theorem ListSlice.mkSlice_roc_eq_mkSlice_rcc {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

(Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rcc.Sliceable.mkSlice xs (lo + 1)...=hi

source

@[simp]

theorem ListSlice.toList_mkSlice_roc {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = List.drop (lo + 1) (List.take (hi + 1) (Std.Slice.toList xs))

source

@[simp]

theorem ListSlice.toArray_mkSlice_roc {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} :

Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = (Std.Slice.toArray xs).extract (lo + 1) (hi + 1)

source

@[simp]

theorem ListSlice.mkSlice_roi_eq_mkSlice_rci {α : Type u_1} {xs : ListSlice α} {lo : Nat} :

Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*

source

@[simp]

theorem ListSlice.toList_mkSlice_roi {α : Type u_1} {xs : ListSlice α} {lo : Nat} :

Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = List.drop (lo + 1) (Std.Slice.toList xs)

source

@[simp]

theorem ListSlice.toArray_mkSlice_roi {α : Type u_1} {xs : ListSlice α} {lo : Nat} :

Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = (Std.Slice.toArray xs).extract (lo + 1)

source

@[simp]

theorem ListSlice.mkSlice_rio_eq_mkSlice_rco {α : Type u_1} {xs : ListSlice α} {hi : Nat} :

(Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi

source

@[simp]

theorem ListSlice.toList_mkSlice_rio {α : Type u_1} {xs : ListSlice α} {hi : Nat} :

Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi (Std.Slice.toList xs)

source

@[simp]

theorem ListSlice.toArray_mkSlice_rio {α : Type u_1} {xs : ListSlice α} {hi : Nat} :

Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = (Std.Slice.toArray xs).extract 0 hi

source

@[simp]

theorem ListSlice.mkSlice_ric_eq_mkSlice_rio {α : Type u_1} {xs : ListSlice α} {hi : Nat} :

(Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1

source

@[simp]

theorem ListSlice.mkSlice_ric_eq_mkSlice_rcc {α : Type u_1} {xs : ListSlice α} {hi : Nat} :

(Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rcc.Sliceable.mkSlice xs 0...=hi

source

@[simp]

theorem ListSlice.toList_mkSlice_ric {α : Type u_1} {xs : ListSlice α} {hi : Nat} :

Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) (Std.Slice.toList xs)

source

@[simp]

theorem ListSlice.toArray_mkSlice_ric {α : Type u_1} {xs : ListSlice α} {hi : Nat} :

Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = (Std.Slice.toArray xs).extract 0 (hi + 1)

source

@[simp]

theorem ListSlice.mkSlice_rii {α : Type u_1} {xs : ListSlice α} :

Std.Rii.Sliceable.mkSlice xs *...* = xs