blob: 31af340006a8a13888701731a2e17067cf763e49 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
|
def BitVec.setBitTrue {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n :=
a ||| BitVec.ofNatLT (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right])
def BitVec.setBitFalse {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n :=
a &&& BitVec.not (BitVec.ofNatLT (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right]))
def BitVec.setBit {n : Nat} (i : Fin n) (v : Bool) (a : BitVec n) : BitVec n :=
if v then
a.setBitTrue i
else
a.setBitFalse i
|
