@[instance_reducible]

instance ByteArray.instLT : LT ByteArray

Equations

• ByteArray.instLT = { lt := fun (a b : ByteArray) => a.data < b.data }

@[instance_reducible]

instance ByteArray.instLE : LE ByteArray

Equations

• ByteArray.instLE = LE.ofLT ByteArray

@[simp]

theorem ByteArray.data_lt_data {a b : ByteArray} : a.data < b.data ↔ a < b

@[extern lean_byte_array_dec_lt]

def ByteArray.decidableLT (a b : ByteArray) : Decidable (a < b)

Equations

• a.decidableLT b = decidable_of_iff (a.data < b.data) ⋯

@[instance_reducible]

instance ByteArray.instDecidableLT : DecidableLT ByteArray

Equations

• ByteArray.instDecidableLT = ByteArray.decidableLT

@[instance_reducible]

instance ByteArray.instDecidableLE : DecidableLE ByteArray

Equations

• a.instDecidableLE b = { decide := !decide (b < a), reflects_decide := ⋯ }

@[extern lean_byte_array_compare]

def ByteArray.compare (a b : ByteArray) : Ordering

Equations

• a.compare b = compare a.data b.data

@[instance_reducible]

instance ByteArray.instOrd : Ord ByteArray

Equations

• ByteArray.instOrd = { compare := ByteArray.compare }

@[simp]

theorem ByteArray.compare_data_data {a b : ByteArray} : compare a.data b.data = compare a b

@[simp]

theorem ByteArray.data_le_data {a b : ByteArray} : a.data ≤ b.data ↔ a ≤ b

@[instance_reducible]

instance ByteArray.instLinearOrderPackage : Std.LinearOrderPackage ByteArray

Equations

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

@[simp]

theorem List.toByteArray_lt_toByteArray {l₁ l₂ : List UInt8} : l₁.toByteArray < l₂.toByteArray ↔ l₁ < l₂

@[simp]

theorem List.toByteArray_le_toByteArray {l₁ l₂ : List UInt8} : l₁.toByteArray ≤ l₂.toByteArray ↔ l₁ ≤ l₂

@[simp]

theorem List.compare_toByteArray_toByteArray {l₁ l₂ : List UInt8} : compare l₁.toByteArray l₂.toByteArray = compare l₁ l₂