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

@[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.2} => 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 }