@[instance_reducible]

instance BitVec.instLinearOrderPackage {w : Nat} : Std.LinearOrderPackage (BitVec w)

Equations

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

@[simp]

theorem BitVec.compare_toNat {w : Nat} {x y : BitVec w} : compare x.toNat y.toNat = compare x y

theorem BitVec.compare_append_append {w v : Nat} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} : compare (x₁ ++ y₁) (x₂ ++ y₂) = (compare x₁ x₂).then (compare y₁ y₂)

theorem BitVec.compare_setWidth_setWidth_of_le {w w' : Nat} {x y : BitVec w} (h : w ≤ w') : compare (setWidth w' x) (setWidth w' y) = compare x y