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 = { internalRepresentation := { 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 = { internalRepresentation := { array := arr.array, start := arr.start, stop := min (arr.start + i) arr.stop, start_le_stop := ⋯, stop_le_array_size := ⋯ } }

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

• s.split i = (s.take ↑i, s.drop ↑i)