diff options
Diffstat (limited to 'Common/BitVec.lean')
| -rw-r--r-- | Common/BitVec.lean | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Common/BitVec.lean b/Common/BitVec.lean new file mode 100644 index 0000000..ad46efb --- /dev/null +++ b/Common/BitVec.lean @@ -0,0 +1,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 |