@[instance_reducible]

instance ByteArray.instLT : LT ByteArray

@[instance_reducible]

instance ByteArray.instLE : LE 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)

@[instance_reducible]

instance ByteArray.instDecidableLT : DecidableLT ByteArray

@[instance_reducible]

instance ByteArray.instDecidableLE : DecidableLE ByteArray

@[extern lean_byte_array_compare]

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

@[instance_reducible]

instance ByteArray.instOrd : Ord ByteArray

@[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

@[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₂