structure Batteries.ByteSubarray : Type

A subarray of a ByteArray.

• array : ByteArray

  O(1). Get data array of a ByteSubarray.

• start : Nat

  O(1). Get start index of a ByteSubarray.

• stop : Nat

  O(1). Get stop index of a ByteSubarray.

• start_le_stop : self.start ≤ self.stop

  Start index is before stop index.

• stop_le_array_size : self.stop ≤ self.array.size

  Stop index is before end of data array.

def Batteries.ByteSubarray.size (self : ByteSubarray) : Nat

O(1). Get the size of a ByteSubarray.

def Batteries.ByteSubarray.isEmpty (self : ByteSubarray) : Bool

O(1). Test if a ByteSubarray is empty.

theorem Batteries.ByteSubarray.stop_eq_start_add_size (self : ByteSubarray) : self.stop = self.start + self.size

def Batteries.ByteSubarray.toByteArray (self : ByteSubarray) : ByteArray

O(n). Extract a ByteSubarray to a ByteArray.

@[inline]

def Batteries.ByteSubarray.get (self : ByteSubarray) (i : Fin self.size) : UInt8

O(1). Get the element at index i from the start of a ByteSubarray.

instance Batteries.ByteSubarray.instGetElemNatUInt8LtSize : GetElem ByteSubarray Nat UInt8 fun (self : ByteSubarray) (i : Nat) => i < self.size

@[inline]

def Batteries.ByteSubarray.pop (self : ByteSubarray) : ByteSubarray

O(1). Pop the last element of a ByteSubarray.

@[inline]

def Batteries.ByteSubarray.popFront (self : ByteSubarray) : ByteSubarray

O(1). Pop the first element of a ByteSubarray.

@[inline]

def Batteries.ByteSubarray.foldlM {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (self : ByteSubarray) (f : β → UInt8 → m β) (init : β) : m β

Folds a monadic function over a ByteSubarray from left to right.

@[inline]

def Batteries.ByteSubarray.foldl {β : Type u_1} (self : ByteSubarray) (f : β → UInt8 → β) (init : β) : β

Folds a function over a ByteSubarray from left to right.

@[specialize #[]]

def Batteries.ByteSubarray.forIn {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (self : ByteSubarray) (init : β) (f : UInt8 → β → m (ForInStep β)) : m β

Implementation of forIn for a ByteSubarray.

def Batteries.ByteSubarray.forIn.loop {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (self : ByteSubarray) (f : UInt8 → β → m (ForInStep β)) (i : Nat) (h : i ≤ self.size) (b : β) : m β

Inner loop of the forIn implementation for ByteSubarray.

instance Batteries.ByteSubarray.instForInUInt8 {m : Type u_1 → Type u_2} : ForIn m ByteSubarray UInt8

instance Batteries.ByteSubarray.instStreamUInt8 : Stream ByteSubarray UInt8

def ByteArray.toByteSubarray (array : ByteArray) : Batteries.ByteSubarray

O(1). Coerce a byte array into a byte slice.

instance instCoeByteArrayByteSubarray : Coe ByteArray Batteries.ByteSubarray