bb9c9bd99f
```lean
@[simp]
theorem shiftLeftRec_zero (x : BitVec w₁) (y : BitVec w₂) :
shiftLeftRec x y 0 = x <<< (y &&& twoPow w₂ 0) := by
simp [shiftLeftRec]
@[simp]
theorem shiftLeftRec_succ (x : BitVec w₁) (y : BitVec w₂) :
shiftLeftRec x y (n + 1) =
(shiftLeftRec x y n) <<< (y &&& twoPow w₂ (n + 1)) := by
simp [shiftLeftRec]
theorem shiftLeftRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) (hn : n + 1 ≤ w₂) :
shiftLeftRec x y n = x <<< (y.truncate (n + 1)).zeroExtend w₂ := by
```
These theorems are used for bitblasting shiftLeft in LeanSAT.
---------
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Kim Morrison <scott@tqft.net>
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
|
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| Bitblast.lean | ||
| Folds.lean | ||
| Lemmas.lean | ||