Documentation

Init.Data.Array.Subarray.Split

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

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

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

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

    Instances For
      def Subarray.split {α : Type u_1} (s : Subarray α) (i : Fin (Std.Slice.size s).succ) :

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

      Instances For