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.

theorem Batteries.ByteSubarray.start_le_stop (self : Batteries.ByteSubarray) : self.start ≤ self.stop

Start index is before stop index.

theorem Batteries.ByteSubarray.stop_le_array_size (self : Batteries.ByteSubarray) : self.stop ≤ self.array.size

Stop index is before end of data array.

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

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

Equations

• self.size = self.stop - self.start

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

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

Equations

• self.isEmpty = (self.start != self.stop)

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

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

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

Equations

• self.toByteArray = self.array.extract self.start self.stop

@[inline]

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

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

Equations

• self.get i = self.array[self.start + ↑i]

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

Equations

• Batteries.ByteSubarray.instGetElemNatUInt8LtSize = { getElem := fun (self : Batteries.ByteSubarray) (i : Nat) (h : i < self.size) => self.get ⟨i, h⟩ }

@[inline]

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

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

Equations

• self.pop = if h : self.start = self.stop then self else { array := self.array, start := self.start, stop := self.stop - 1, start_le_stop := ⋯, stop_le_array_size := ⋯ }

@[inline]

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

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

Equations

• self.popFront = if h : self.start = self.stop then self else { array := self.array, start := self.start + 1, stop := self.stop, start_le_stop := ⋯, stop_le_array_size := ⋯ }

@[inline]

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

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

Equations

• self.foldlM f init = ByteArray.foldlM f init self.array self.start self.stop

@[inline]

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

Folds a function over a ByteSubarray from left to right.

Equations

• self.foldl f init = self.foldlM f init

@[specialize #[]]

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

Implementation of forIn for a ByteSubarray.

Equations

• self.forIn init f = Batteries.ByteSubarray.forIn.loop self f self.size ⋯ init

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

Inner loop of the forIn implementation for ByteSubarray.

Equations

• One or more equations did not get rendered due to their size.
• Batteries.ByteSubarray.forIn.loop self f 0 x b = pure b

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

Equations

• Batteries.ByteSubarray.instForInUInt8 = { forIn := fun {β : Type ?u.14} [Monad m] => Batteries.ByteSubarray.forIn }

instance Batteries.ByteSubarray.instStreamUInt8 : Stream Batteries.ByteSubarray UInt8

Equations

• Batteries.ByteSubarray.instStreamUInt8 = { next? := fun (s : Batteries.ByteSubarray) => do let x ← s[0]? some (x, s.popFront) }

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

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

Equations

• array.toByteSubarray = { array := array, start := 0, stop := array.size, start_le_stop := ⋯, stop_le_array_size := ⋯ }

instance instCoeByteArrayByteSubarray : Coe ByteArray Batteries.ByteSubarray

Equations

• instCoeByteArrayByteSubarray = { coe := ByteArray.toByteSubarray }