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

A well-ordered relation for "upwards" induction on the natural numbers up to some bound 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.

structure ByteSliceT : Type

• arr : ByteArray
• off : ℕ

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

@[inline]

def ByteSliceT.size (self : ByteSliceT) : ℕ

The number of elements in the byte slice.

@[inline]

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

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

def ByteArray.toSliceT (arr : ByteArray) : ByteSliceT

Convert a byte array into a terminal slice.

structure ByteSlice : Type

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

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

def ByteSlice.toArray : ByteSlice → ByteArray

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

@[inline]

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

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

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

def ByteSliceT.toSlice : ByteSliceT → ByteSlice

Convert a terminal byte slice into a regular byte slice.

def ByteArray.toSlice (arr : ByteArray) : ByteSlice

Convert a byte array into a byte slice.

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

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.

instance instToStringByteSlice : ToString ByteSlice