@[reducible, inline]

abbrev ByteSlice.isEmpty (s : ByteSlice) : Bool

Test whether a byte slice is empty.

theorem ByteSlice.stop_eq_start_add_size (s : ByteSlice) : s.stop = s.start + s.size

@[reducible, inline]

abbrev ByteSlice.pop (s : ByteSlice) : ByteSlice

Returns the subslice obtained by removing the last element.

@[reducible, inline]

abbrev ByteSlice.popFront (s : ByteSlice) : ByteSlice

Returns the subslice obtained by removing the first element.

@[inline]

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

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

@[inline]

def ByteSlice.foldl {β : Type u_1} (s : ByteSlice) (f : β → UInt8 → β) (init : β) : β

Folds a function over a ByteSubarray from left to right.

@[specialize #[]]

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

Implementation of forIn for a ByteSlice.

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

Inner loop of the forIn implementation for ByteSlice.

@[implicit_reducible]

instance ByteSlice.instForInUInt8OfMonad_batteries {m : Type u_1 → Type u_2} [Monad m] : ForIn m ByteSlice UInt8

@[implicit_reducible]

instance ByteSlice.instStreamUInt8_batteries : Std.Stream ByteSlice UInt8

@[implicit_reducible]

instance ByteSlice.instCoeByteArray_batteries : Coe ByteArray ByteSlice

@[deprecated ByteSlice (since := "2025-10-04")]

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.

@[deprecated ByteSlice.size (since := "2025-10-04")]

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

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

@[deprecated ByteSlice.isEmpty (since := "2025-10-04")]

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

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

@[deprecated ByteSlice.stop_eq_start_add_size (since := "2025-10-04")]

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

@[deprecated ByteSlice.toByteArray (since := "2025-10-04")]

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

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

@[inline, deprecated ByteSlice.get (since := "2025-10-04")]

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.

@[implicit_reducible]

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

@[inline, deprecated ByteSlice.pop (since := "2025-10-04")]

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

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

@[inline, deprecated ByteSlice.popFront (since := "2025-10-04")]

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

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

@[inline, deprecated ByteSlice.foldlM (since := "2025-10-04")]

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, deprecated ByteSlice.foldl (since := "2025-10-04")]

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.

@[implicit_reducible]

instance Batteries.ByteSubarray.instForInUInt8OfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m ByteSubarray UInt8

@[implicit_reducible]

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

@[deprecated ByteArray.toByteSlice (since := "2025-10-04")]

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

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

@[implicit_reducible]

instance instCoeByteArrayByteSubarray : Coe ByteArray Batteries.ByteSubarray