source
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 := ⋯ } }

Instances For

source
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 := ⋯ } }

Instances For

source
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)

Instances For