@[simp]

theorem LLVM.lshr?_eq_some {w : ℕ} {a : BitVec w} {b : BitVec w} (hb : b < ↑w) : LLVM.lshr? a b = some (a.ushiftRight b.toNat)

Note that this assumes that the input and output bitwidths are the same, which is by far the common case.

@[simp]

theorem LLVM.lshr?_eq_none {w : ℕ} {a : BitVec w} {b : BitVec w} (hb : b ≥ ↑w) : LLVM.lshr? a b = none

Note that this assumes that the input and output bitwidths are the same, which is by far the common case.

@[simp]

theorem LLVM.select?_eq_none {w : ℕ} {a : LLVM.IntW w} {b : LLVM.IntW w} : LLVM.select none a b = none

@[simp]

theorem LLVM.select?_some_true {w : ℕ} {a : LLVM.IntW w} {b : LLVM.IntW w} : LLVM.select (some (BitVec.ofBool true)) a b = a

@[simp]

theorem LLVM.select?_some_false {w : ℕ} {a : LLVM.IntW w} {b : LLVM.IntW w} : LLVM.select (some (BitVec.ofBool false)) a b = b

@[simp]

theorem LLVM.select?_eq_some {w : ℕ} {c : BitVec 1} {x : Option (BitVec w)} {y : Option (BitVec w)} : LLVM.select (some c) x y = if c = 1 then x else y

@[simp]

theorem LLVM.sdiv?_denom_zero {w : ℕ} {a : BitVec w} {b : BitVec w} (hb : b = 0) : LLVM.sdiv? a b = none