blob: ad46efbe3d444127d6f6a6af9904b0993e6d79fb (
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
|
