# Documentation

Mathlib.Data.ByteArray

def Nat.Up (ub : ) (a : ) (i : ) :

A well-ordered relation for "upwards" induction on the natural numbers up to some bound ub.

Instances For
theorem Nat.Up.next {ub : } {i : } (h : i < ub) :
Nat.Up ub (i + 1) i
theorem Nat.Up.WF (ub : ) :
def Nat.upRel (ub : ) :

A well-ordered relation for "upwards" induction on the natural numbers up to some bound ub.

Instances For
structure ByteSliceT :

A terminal byte slice, a suffix of a byte array.

Instances For
@[inline]

The number of elements in the byte slice.

Instances For
@[inline]
def ByteSliceT.getOp (self : ByteSliceT) (idx : ) :

Index into a byte slice. The getOp function allows the use of the buf[i] notation.

Instances For

Convert a byte array into a terminal slice.

Instances For
structure ByteSlice :

A byte slice, given by a backing byte array, and an offset and length.

Instances For

Convert a byte slice into an array, by copying the data if necessary.

Instances For
@[inline]
def ByteSlice.getOp (self : ByteSlice) (idx : ) :

Index into a byte slice. The getOp function allows the use of the buf[i] notation.

Instances For
def ByteSlice.forIn.loop {m : Type u_1 → Type u_2} {β : Type u_1} [] (f : UInt8βm ()) (arr : ByteArray) (off : ) (_end : ) (i : ) (b : β) :
m β

The inner loop of the forIn implementation for byte slices.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Convert a terminal byte slice into a regular byte slice.

Instances For

Convert a byte array into a byte slice.

Instances For

Convert a string of assumed-ASCII characters into a byte array. (If any characters are non-ASCII they will be reduced modulo 256.)

Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For

Convert a byte slice into a string. This does not handle non-ASCII characters correctly: every byte will become a unicode character with codepoint < 256.

Instances For