# 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.

Equations
• ub.Up a i = (i < a i < ub)
Instances For
theorem Nat.Up.next {ub : } {i : } (h : i < ub) :
ub.Up (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.

Equations
• ub.upRel = { rel := ub.Up, wf := }
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.

Equations
• self.size = self.arr.size - self.off
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.

Equations
• self.getOp idx = self.arr.get! (self.off + idx)
Instances For

Convert a byte array into a terminal slice.

Equations
• arr.toSliceT = { arr := arr, off := 0 }
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.

Equations
• x.toArray = match x with | { arr := arr, off := off, len := len } => arr.extract off len
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.

Equations
• self.getOp idx = self.arr.get! (self.off + idx)
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
instance ByteSlice.instForInUInt8 {m : Type u_1 → Type u_2} :
Equations
• One or more equations did not get rendered due to their size.

Convert a terminal byte slice into a regular byte slice.

Equations
• x.toSlice = match x with | { arr := arr, off := off } => { arr := arr, off := off, len := arr.size - off }
Instances For

Convert a byte array into a byte slice.

Equations
• arr.toSlice = { arr := arr, off := 0, len := arr.size }
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.)

Equations
• s.toAsciiByteArray =
Instances For
Equations
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.

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