5f3c0daf3d
This PR supports rewriting `ushiftRight` in terms of `extractLsb'`. This is the companion PR to #6743 which adds the similar lemmas about `shiftLeft`. ```lean theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) : x >>> n = 0#w theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) : x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega) ``` |
||
|---|---|---|
| .. | ||
| bin | ||
| cmake | ||
| include/lean | ||
| Init | ||
| initialize | ||
| kernel | ||
| lake | ||
| Lean | ||
| library | ||
| runtime | ||
| shell | ||
| Std | ||
| util | ||
| cadical.mk | ||
| CMakeLists.txt | ||
| config.h.in | ||
| githash.h.in | ||
| Init.lean | ||
| lakefile.toml.in | ||
| lean-toolchain | ||
| Lean.lean | ||
| lean.mk.in | ||
| Leanc.lean | ||
| Std.lean | ||
| stdlib.make.in | ||
| stdlib_flags.h | ||
| version.h.in | ||