Documentation

Init.Data.Slice.Array.Lemmas

source
instance Subarray.instLawfulSliceSizeSubarrayIteratorSubarrayData {α : Type u_1} :
Std.Slice.LawfulSliceSize (Std.Slice.Internal.SubarrayData α)
source
theorem Subarray.toArray_eq_sliceToArray {α : Type u} {s : Subarray α} :
↑s = Std.Slice.toArray s
source
@[simp]
theorem Subarray.forIn_toList {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ} {f : α → γ → m (ForInStep γ)} :
ForIn.forIn (Std.Slice.toList s) init f = ForIn.forIn s init f
source
@[simp]
theorem Subarray.forIn_toArray {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ} {f : α → γ → m (ForInStep γ)} :
ForIn.forIn (↑s) init f = ForIn.forIn s init f
source
theorem Array.toSubarray_eq_toSubarray_of_min_eq_min {α : Type u_1} {xs : Array α} {start stop stop' : Nat} (h : min stop xs.size = min stop' xs.size) :
xs.toSubarray start stop = xs.toSubarray start stop'
source
theorem Array.toSubarray_eq_min {α : Type u_1} {xs : Array α} {lo hi : Nat} :
xs.toSubarray lo hi = { internalRepresentation := { array := xs, start := min lo (min hi xs.size), stop := min hi xs.size, start_le_stop := ⋯, stop_le_array_size := ⋯ } }
source
@[simp]
theorem Array.array_toSubarray {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(xs.toSubarray lo hi).array = xs
source
@[simp]
theorem Array.start_toSubarray {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(xs.toSubarray lo hi).start = min lo (min hi xs.size)
source
@[simp]
theorem Array.stop_toSubarray {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(xs.toSubarray lo hi).stop = min hi xs.size
source
theorem Subarray.size_eq {α : Type u_1} {xs : Subarray α} :
xs.size = xs.stop - xs.start
source
@[simp]
theorem Subarray.toArray_toList {α : Type u_1} {xs : Subarray α} :
(Std.Slice.toList xs).toArray = ↑xs
source
@[simp]
theorem Subarray.toList_toArray {α : Type u_1} {xs : Subarray α} :
(↑xs).toList = Std.Slice.toList xs
source
@[simp]
theorem Subarray.length_toList {α : Type u_1} {xs : Subarray α} :
(Std.Slice.toList xs).length = xs.size
source
@[simp]
theorem Subarray.size_toArray {α : Type u_1} {xs : Subarray α} :
(↑xs).size = xs.size
source
@[simp]
theorem Array.array_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rco.Sliceable.mkSlice xs lo...hi).array = xs
source
@[simp]
theorem Array.start_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rco.Sliceable.mkSlice xs lo...hi).start = min lo (min hi xs.size)
source
@[simp]
theorem Array.stop_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rco.Sliceable.mkSlice xs lo...hi).stop = min hi xs.size
source
theorem Array.mkSlice_rco_eq_mkSlice_rco_min {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rco.Sliceable.mkSlice xs lo...hi) = Std.Rco.Sliceable.mkSlice xs (min lo (min hi xs.size))...min hi xs.size
source
@[simp]
theorem Array.toList_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} :
Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...hi) = List.drop lo (List.take hi xs.toList)
source
@[simp]
theorem Array.toArray_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} :
↑(Std.Rco.Sliceable.mkSlice xs lo...hi) = xs.extract lo hi
source
@[simp]
theorem Array.size_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rco.Sliceable.mkSlice xs lo...hi).size = min hi xs.size - lo
source
@[simp]
theorem Array.mkSlice_rcc_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1
source
theorem Array.mkSlice_rcc_eq_mkSlice_rco_min {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs (min lo (min (hi + 1) xs.size))...min (hi + 1) xs.size
source
@[simp]
theorem Array.array_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rcc.Sliceable.mkSlice xs lo...=hi).array = xs
source
@[simp]
theorem Array.start_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rcc.Sliceable.mkSlice xs lo...=hi).start = min lo (min (hi + 1) xs.size)
source
@[simp]
theorem Array.stop_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rcc.Sliceable.mkSlice xs lo...=hi).stop = min (hi + 1) xs.size
source
@[simp]
theorem Array.toList_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = List.drop lo (List.take (hi + 1) xs.toList)
source
@[simp]
theorem Array.toArray_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
↑(Std.Rcc.Sliceable.mkSlice xs lo...=hi) = xs.extract lo (hi + 1)
source
@[simp]
theorem Array.size_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Rcc.Sliceable.mkSlice xs lo...=hi).size = min (hi + 1) xs.size - lo
source
@[simp]
theorem Array.array_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} :
(Std.Rci.Sliceable.mkSlice xs lo...*).array = xs
source
@[simp]
theorem Array.start_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} :
(Std.Rci.Sliceable.mkSlice xs lo...*).start = min lo xs.size
source
@[simp]
theorem Array.stop_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} :
(Std.Rci.Sliceable.mkSlice xs lo...*).stop = xs.size
source
@[simp]
theorem Array.mkSlice_rci_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {lo : Nat} :
Std.Rci.Sliceable.mkSlice xs lo...* = Std.Rco.Sliceable.mkSlice xs lo...xs.size
source
theorem Array.mkSlice_rci_eq_mkSlice_rco_min {α : Type u_1} {xs : Array α} {lo : Nat} :
Std.Rci.Sliceable.mkSlice xs lo...* = Std.Rco.Sliceable.mkSlice xs (min lo xs.size)...xs.size
source
@[simp]
theorem Array.toList_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} :
Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = List.drop lo xs.toList
source
@[simp]
theorem Array.toArray_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} :
↑(Std.Rci.Sliceable.mkSlice xs lo...*) = xs.extract lo
source
@[simp]
theorem Array.size_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} :
(Std.Rci.Sliceable.mkSlice xs lo...*).size = xs.size - lo
source
@[simp]
theorem Array.array_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roo.Sliceable.mkSlice xs lo<...hi).array = xs
source
@[simp]
theorem Array.start_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roo.Sliceable.mkSlice xs lo<...hi).start = min (lo + 1) (min hi xs.size)
source
@[simp]
theorem Array.stop_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roo.Sliceable.mkSlice xs lo<...hi).stop = min hi xs.size
source
@[simp]
theorem Array.mkSlice_roo_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi
source
theorem Array.mkSlice_roo_eq_mkSlice_roo_min {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (min (lo + 1) (min hi xs.size))...min hi xs.size
source
@[simp]
theorem Array.toList_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} :
Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...hi) = List.drop (lo + 1) (List.take hi xs.toList)
source
@[simp]
theorem Array.toArray_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} :
↑(Std.Roo.Sliceable.mkSlice xs lo<...hi) = xs.extract (lo + 1) hi
source
@[simp]
theorem Array.size_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roo.Sliceable.mkSlice xs lo<...hi).size = min hi xs.size - (lo + 1)
source
@[simp]
theorem Array.array_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roc.Sliceable.mkSlice xs lo<...=hi).array = xs
source
@[simp]
theorem Array.start_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roc.Sliceable.mkSlice xs lo<...=hi).start = min (lo + 1) (min (hi + 1) xs.size)
source
@[simp]
theorem Array.stop_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roc.Sliceable.mkSlice xs lo<...=hi).stop = min (hi + 1) xs.size
source
@[simp]
theorem Array.mkSlice_roc_eq_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1
source
theorem Array.mkSlice_roc_eq_mkSlice_roo_min {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (min (lo + 1) (min (hi + 1) xs.size))...min (hi + 1) xs.size
source
@[simp]
theorem Array.toList_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = List.drop (lo + 1) (List.take (hi + 1) xs.toList)
source
@[simp]
theorem Array.toArray_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
↑(Std.Roc.Sliceable.mkSlice xs lo<...=hi) = xs.extract (lo + 1) (hi + 1)
source
@[simp]
theorem Array.size_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} :
(Std.Roc.Sliceable.mkSlice xs lo<...=hi).size = min (hi + 1) xs.size - (lo + 1)
source
@[simp]
theorem Array.array_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} :
(Std.Roi.Sliceable.mkSlice xs lo<...*).array = xs
source
@[simp]
theorem Array.start_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} :
(Std.Roi.Sliceable.mkSlice xs lo<...*).start = min (lo + 1) xs.size
source
@[simp]
theorem Array.stop_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} :
(Std.Rci.Sliceable.mkSlice xs lo...*).stop = xs.size
source
@[simp]
theorem Array.mkSlice_roi_eq_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} :
Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*
source
theorem Array.mkSlice_roi_eq_mkSlice_roo {α : Type u_1} {xs : Array α} {lo : Nat} :
Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Roo.Sliceable.mkSlice xs lo<...xs.size
source
theorem Array.mkSlice_roi_eq_mkSlice_roo_min {α : Type u_1} {xs : Array α} {lo : Nat} :
Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rco.Sliceable.mkSlice xs (min (lo + 1) xs.size)...xs.size
source
@[simp]
theorem Array.toList_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} :
Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = List.drop (lo + 1) xs.toList
source
@[simp]
theorem Array.toArray_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} :
↑(Std.Roi.Sliceable.mkSlice xs lo<...*) = xs.drop (lo + 1)
source
@[simp]
theorem Array.size_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} :
(Std.Roi.Sliceable.mkSlice xs lo<...*).size = xs.size - (lo + 1)
source
@[simp]
theorem Array.array_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Rio.Sliceable.mkSlice xs *...hi).array = xs
source
@[simp]
theorem Array.start_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Rio.Sliceable.mkSlice xs *...hi).start = 0
source
@[simp]
theorem Array.stop_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Rio.Sliceable.mkSlice xs *...hi).stop = min hi xs.size
source
@[simp]
theorem Array.mkSlice_rio_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi
source
theorem Array.mkSlice_rio_eq_mkSlice_rio_min {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rio.Sliceable.mkSlice xs *...min hi xs.size
source
@[simp]
theorem Array.toList_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} :
Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi xs.toList
source
@[simp]
theorem Array.toArray_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} :
↑(Std.Rio.Sliceable.mkSlice xs *...hi) = xs.extract 0 hi
source
@[simp]
theorem Array.size_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Rio.Sliceable.mkSlice xs *...hi).size = min hi xs.size
source
@[simp]
theorem Array.array_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Ric.Sliceable.mkSlice xs *...=hi).array = xs
source
@[simp]
theorem Array.start_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Ric.Sliceable.mkSlice xs *...=hi).start = 0
source
@[simp]
theorem Array.stop_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Ric.Sliceable.mkSlice xs *...=hi).stop = min (hi + 1) xs.size
source
@[simp]
theorem Array.mkSlice_ric_eq_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1
source
theorem Array.mkSlice_ric_eq_mkSlice_rio_min {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...min (hi + 1) xs.size
source
@[simp]
theorem Array.toList_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} :
Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) xs.toList
source
@[simp]
theorem Array.toArray_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} :
↑(Std.Ric.Sliceable.mkSlice xs *...=hi) = xs.extract 0 (hi + 1)
source
@[simp]
theorem Array.size_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} :
(Std.Ric.Sliceable.mkSlice xs *...=hi).size = min (hi + 1) xs.size
source
@[simp]
theorem Array.mkSlice_rii_eq_mkSlice_rci {α : Type u_1} {xs : Array α} :
Std.Rii.Sliceable.mkSlice xs *...* = Std.Rci.Sliceable.mkSlice xs 0...*
source
theorem Array.mkSlice_rii_eq_mkSlice_rio {α : Type u_1} {xs : Array α} :
Std.Rii.Sliceable.mkSlice xs *...* = Std.Rio.Sliceable.mkSlice xs *...xs.size
source
theorem Array.mkSlice_rii_eq_mkSlice_rio_min {α : Type u_1} {xs : Array α} :
Std.Rii.Sliceable.mkSlice xs *...* = Std.Rio.Sliceable.mkSlice xs *...xs.size
source
@[simp]
theorem Array.toList_mkSlice_rii {α : Type u_1} {xs : Array α} :
Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = xs.toList
source
@[simp]
theorem Array.toArray_mkSlice_rii {α : Type u_1} {xs : Array α} :
↑(Std.Rii.Sliceable.mkSlice xs *...*) = xs
source
@[simp]
theorem Array.size_mkSlice_rii {α : Type u_1} {xs : Array α} :
(Std.Rii.Sliceable.mkSlice xs *...*).size = xs.size
source
@[simp]
theorem Array.array_mkSlice_rii {α : Type u_1} {xs : Array α} :
(Std.Rii.Sliceable.mkSlice xs *...*).array = xs
source
@[simp]
theorem Array.start_mkSlice_rii {α : Type u_1} {xs : Array α} :
(Std.Rii.Sliceable.mkSlice xs *...*).start = 0
source
@[simp]
theorem Array.stop_mkSlice_rii {α : Type u_1} {xs : Array α} :
(Std.Rii.Sliceable.mkSlice xs *...*).stop = xs.size
source
@[simp]
theorem Subarray.toList_mkSlice_rco {α : Type u_1} {xs : Subarray α} {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 Subarray.toArray_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo hi : Nat} :
↑(Std.Rco.Sliceable.mkSlice xs lo...hi) = (↑xs).extract lo hi
source
@[simp]
theorem Subarray.mkSlice_rcc_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo hi : Nat} :
(Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1
source
@[simp]
theorem Subarray.toList_mkSlice_rcc {α : Type u_1} {xs : Subarray α} {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 Subarray.toArray_mkSlice_rcc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} :
↑(Std.Rcc.Sliceable.mkSlice xs lo...=hi) = (↑xs).extract lo (hi + 1)
source
@[simp]
theorem Subarray.mkSlice_rci_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo : Nat} :
Std.Rci.Sliceable.mkSlice xs lo...* = Std.Rco.Sliceable.mkSlice xs lo...xs.size
source
@[simp]
theorem Subarray.toList_mkSlice_rci {α : Type u_1} {xs : Subarray α} {lo : Nat} :
Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = List.drop lo (Std.Slice.toList xs)
source
@[simp]
theorem Subarray.toArray_mkSlice_rci {α : Type u_1} {xs : Subarray α} {lo : Nat} :
↑(Std.Rci.Sliceable.mkSlice xs lo...*) = (↑xs).extract lo
source
@[simp]
theorem Subarray.mkSlice_roc_eq_mkSlice_roo {α : Type u_1} {xs : Subarray α} {lo hi : Nat} :
(Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1
source
@[simp]
theorem Subarray.mkSlice_roo_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo hi : Nat} :
(Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi
source
@[simp]
theorem Subarray.toList_mkSlice_roo {α : Type u_1} {xs : Subarray α} {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 Subarray.toArray_mkSlice_roo {α : Type u_1} {xs : Subarray α} {lo hi : Nat} :
↑(Std.Roo.Sliceable.mkSlice xs lo<...hi) = (↑xs).extract (lo + 1) hi
source
@[simp]
theorem Subarray.mkSlice_roc_eq_mkSlice_rcc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} :
(Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rcc.Sliceable.mkSlice xs (lo + 1)...=hi
source
@[simp]
theorem Subarray.toList_mkSlice_roc {α : Type u_1} {xs : Subarray α} {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 Subarray.toArray_mkSlice_roc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} :
↑(Std.Roc.Sliceable.mkSlice xs lo<...=hi) = (↑xs).extract (lo + 1) (hi + 1)
source
@[simp]
theorem Subarray.mkSlice_roi_eq_mkSlice_rci {α : Type u_1} {xs : Subarray α} {lo : Nat} :
Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*
source
@[simp]
theorem Subarray.toList_mkSlice_roi {α : Type u_1} {xs : Subarray α} {lo : Nat} :
Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = List.drop (lo + 1) (Std.Slice.toList xs)
source
@[simp]
theorem Subarray.toArray_mkSlice_roi {α : Type u_1} {xs : Subarray α} {lo : Nat} :
↑(Std.Roi.Sliceable.mkSlice xs lo<...*) = (↑xs).extract (lo + 1)
source
@[simp]
theorem Subarray.mkSlice_ric_eq_mkSlice_rio {α : Type u_1} {xs : Subarray α} {hi : Nat} :
(Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1
source
@[simp]
theorem Subarray.mkSlice_rio_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {hi : Nat} :
(Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi
source
@[simp]
theorem Subarray.toList_mkSlice_rio {α : Type u_1} {xs : Subarray α} {hi : Nat} :
Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi (Std.Slice.toList xs)
source
@[simp]
theorem Subarray.toArray_mkSlice_rio {α : Type u_1} {xs : Subarray α} {hi : Nat} :
↑(Std.Rio.Sliceable.mkSlice xs *...hi) = (↑xs).extract 0 hi
source
@[simp]
theorem Subarray.mkSlice_ric_eq_mkSlice_rcc {α : Type u_1} {xs : Subarray α} {hi : Nat} :
(Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rcc.Sliceable.mkSlice xs 0...=hi
source
@[simp]
theorem Subarray.toList_mkSlice_ric {α : Type u_1} {xs : Subarray α} {hi : Nat} :
Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) (Std.Slice.toList xs)
source
@[simp]
theorem Subarray.toArray_mkSlice_ric {α : Type u_1} {xs : Subarray α} {hi : Nat} :
↑(Std.Ric.Sliceable.mkSlice xs *...=hi) = (↑xs).extract 0 (hi + 1)
source
@[simp]
theorem Subarray.mkSlice_rii {α : Type u_1} {xs : Subarray α} :
Std.Rii.Sliceable.mkSlice xs *...* = xs
source
@[simp]
theorem Subarray.toList_mkSlice_rii {α : Type u_1} {xs : Subarray α} :
Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = Std.Slice.toList xs
source
@[simp]
theorem Subarray.toArray_mkSlice_rii {α : Type u_1} {xs : Subarray α} :
↑(Std.Rii.Sliceable.mkSlice xs *...*) = ↑xs