We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 00cc525 commit 2bcf81fCopy full SHA for 2bcf81f
src/Init/Data/BitVec/Bitblast.lean
@@ -1767,7 +1767,7 @@ theorem umod_msb_false {x y : BitVec w} (xmsb : y.msb = false) (hy_ne_zero : y
1767
exact le_of_msb_true_of_msb_false xmsb h
1768
1769
@[simp]
1770
-theorem intMin_umod_msb_false {y : BitVec w} (hy : y.msb = true) (hy_ne_zero : y ≠ 0#w):
+theorem intMin_umod_msb_false {y : BitVec w} (hy : y.msb = true) (hy_ne_zero : y ≠ 0#w) :
1771
(intMin w % (-y)).msb = false := by
1772
by_cases yintmin : y = intMin w
1773
· simp [yintmin]
0 commit comments