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.

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.

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.