def BitVec.set {w : Nat} (b : BitVec w) (i : Nat) : BitVec w

Equations

• b.set i = if i < w then b ||| ↑(1 <<< i) else b

@[simp]

theorem BitVec.set_lt {w : Nat} (b : BitVec w) (i : Nat) (h : i < w) : b.set i = b ||| ↑(1 <<< i)

theorem BitVec.getElem_set_eq {w : Nat} (b : BitVec w) (i : Nat) (h : i < w) : (b.set i)[i] = true

theorem BitVec.getElem_set_ne {w : Nat} (b : BitVec w) (i j : Nat) (h : i < w) (h' : j < w) (hne : i ≠ j) : (b.set i)[j] = b[j]

def BitVec.popcount {w : Nat} (b : BitVec w) : Nat

Equations

• b.popcount = b.toNat.popcount

theorem BitVec.popcount_set_not_getElem {w : Nat} (b : BitVec w) (i : Nat) (h : i < w) (h' : ¬b[i] = true) : (b.set i).popcount = b.popcount + 1

theorem BitVec.popcount_le {w : Nat} (b : BitVec w) : b.popcount ≤ w

theorem BitVec.sub_lt_popcount_set_not_getElem {w : Nat} (b : BitVec w) (i : Nat) (h : i < w) (h' : ¬b[i] = true) : w + 1 - (b.set i).popcount < w + 1 - b.popcount