diff options
| author | Andreas Grois <andi@grois.info> | 2024-12-14 00:09:46 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-12-14 00:09:46 +0100 |
| commit | 8223584095273bc7bdf7b7dc65a6e168350cdf57 (patch) | |
| tree | 2934a22693564082e78d896d98769e0ddc0e9996 /Common/BitVec.lean | |
| parent | 4784df61d4858f9f470327e46822aabf2f7eff52 (diff) | |
Begin Day16
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 |