@[reducible, inline]

abbrev ByteSlice.isEmpty (s : ByteSlice) : Bool

Test whether a byte slice is empty.

Equations

• s.isEmpty = (s.start == s.stop)

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.

Equations

• s.pop = s.slice 0 (s.size - 1)

@[reducible, inline]

abbrev ByteSlice.popFront (s : ByteSlice) : ByteSlice

Returns the subslice obtained by removing the first element.

Equations

• s.popFront = s.slice 1

@[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.

Equations

• s.foldlM f init = ByteArray.foldlM f init s.toByteArray s.start s.stop

@[inline]

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

Folds a function over a ByteSubarray from left to right.

Equations

• s.foldl f init = s.foldlM f init

@[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.

Equations

• s.forIn init f = ByteSlice.forIn.loop s f s.size ⋯ init

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.

Equations

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

@[implicit_reducible]

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

Equations

• ByteSlice.instForInUInt8OfMonad_batteries = { forIn := fun {β : Type ?u.14} => ByteSlice.forIn }

@[implicit_reducible]

instance ByteSlice.instStreamUInt8_batteries : Std.Stream ByteSlice UInt8

Equations

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

@[implicit_reducible]

instance ByteSlice.instCoeByteArray_batteries : Coe ByteArray ByteSlice

Equations

• ByteSlice.instCoeByteArray_batteries = { coe := fun (as : ByteArray) => as.toByteSlice }

@[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.

Equations

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

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

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

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

Equations

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

@[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.

Equations

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

@[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.

Equations

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

@[implicit_reducible]

instance Batteries.ByteSubarray.instGetElemNatUInt8LtSize : GetElem ByteSubarray Nat UInt8 fun (self : 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, deprecated ByteSlice.pop (since := "2025-10-04")]

def Batteries.ByteSubarray.pop (self : ByteSubarray) : 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, deprecated ByteSlice.popFront (since := "2025-10-04")]

def Batteries.ByteSubarray.popFront (self : ByteSubarray) : 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, 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.

Equations

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

@[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.

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 : 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 : 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

@[implicit_reducible]

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

Equations

• Batteries.ByteSubarray.instForInUInt8OfMonad = { forIn := fun {β : Type ?u.14} => Batteries.ByteSubarray.forIn }

@[implicit_reducible]

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

Equations

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

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

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

@[implicit_reducible]

instance instCoeByteArrayByteSubarray : Coe ByteArray Batteries.ByteSubarray

Equations

• instCoeByteArrayByteSubarray = { coe := ByteArray.toByteSubarray }