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

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

Equations

• Nat.Up ub a i = (i < a ∧ i < ub)

theorem Nat.Up.next {ub : ℕ} {i : ℕ} (h : i < ub) : Nat.Up ub (i + 1) i

theorem Nat.Up.WF (ub : ℕ) : WellFounded (Nat.Up ub)

def Nat.upRel (ub : ℕ) : WellFoundedRelation ℕ

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

Equations

• Nat.upRel ub = { rel := Nat.Up ub, wf := (_ : WellFounded (Nat.Up ub)) }

structure ByteSliceT : Type

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

• arr : ByteArray
• off : ℕ

@[inline]

def ByteSliceT.size (self : ByteSliceT) : ℕ

The number of elements in the byte slice.

Equations

• ByteSliceT.size self = ByteArray.size self.arr - self.off

@[inline]

def ByteSliceT.getOp (self : ByteSliceT) (idx : ℕ) : UInt8

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

Equations

• ByteSliceT.getOp self idx = ByteArray.get! self.arr (self.off + idx)

def ByteArray.toSliceT (arr : ByteArray) : ByteSliceT

Convert a byte array into a terminal slice.

Equations

• ByteArray.toSliceT arr = { arr := arr, off := 0 }

structure ByteSlice : Type

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

• arr : ByteArray
• off : ℕ
• len : ℕ

def ByteSlice.toArray : ByteSlice → ByteArray

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

Equations

• ByteSlice.toArray x = match x with | { arr := arr, off := off, len := len } => ByteArray.extract arr off len

@[inline]

def ByteSlice.getOp (self : ByteSlice) (idx : ℕ) : UInt8

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

Equations

• ByteSlice.getOp self idx = ByteArray.get! self.arr (self.off + idx)

def ByteSlice.forIn.loop {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : UInt8 → β → m (ForInStep β)) (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.

instance ByteSlice.instForInByteSliceUInt8 {m : Type u_1 → Type u_2} : ForIn m ByteSlice UInt8

Equations

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

def ByteSliceT.toSlice : ByteSliceT → ByteSlice

Convert a terminal byte slice into a regular byte slice.

Equations

• ByteSliceT.toSlice x = match x with | { arr := arr, off := off } => { arr := arr, off := off, len := ByteArray.size arr - off }

def ByteArray.toSlice (arr : ByteArray) : ByteSlice

Convert a byte array into a byte slice.

Equations

• ByteArray.toSlice arr = { arr := arr, off := 0, len := ByteArray.size arr }

def String.toAsciiByteArray (s : String) : ByteArray

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

Equations

• String.toAsciiByteArray s = String.toAsciiByteArray.loop s 0 ByteArray.empty

def String.toAsciiByteArray.loop (s : String) (p : String.Pos) (out : ByteArray) : ByteArray

Equations

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

def ByteSlice.toString (bs : ByteSlice) : String

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.

instance instToStringByteSlice : ToString ByteSlice

Equations

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