def Subarray.split {α : Type u_1} (s : Subarray α) (i : Fin s.size.succ) : Subarray α × Subarray α

Splits a subarray into two parts, the first of which contains the first i elements and the second of which contains the remainder.

Equations

• One or more equations did not get rendered due to their size.

def Subarray.drop {α : Type u_1} (arr : Subarray α) (i : Nat) : Subarray α

Removes the first i elements of the subarray. If there are i or fewer elements, the resulting subarray is empty.

Equations

• arr.drop i = { array := arr.array, start := min (arr.start + i) arr.stop, stop := arr.stop, start_le_stop := ⋯, stop_le_array_size := ⋯ }

def Subarray.take {α : Type u_1} (arr : Subarray α) (i : Nat) : Subarray α

Keeps only the first i elements of the subarray. If there are i or fewer elements, the resulting subarray is empty.

Equations

• arr.take i = { array := arr.array, start := arr.start, stop := min (arr.start + i) arr.stop, start_le_stop := ⋯, stop_le_array_size := ⋯ }