test: adapt test for arbitrary shiftRight

leanprover · Aug 1, 2024 · 20ff265 · 20ff265
1 parent d71085f
commit 20ff265
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Test/Bv/Shift.lean b/Test/Bv/Shift.lean
@@ -26,9 +26,8 @@ set_option trace.bv true in
 theorem shift_unit_5 {x y z : BitVec 16} : (x <<< y) <<< z = (x <<< z) <<< y := by
   bv_decide
 
--- This demonstrates we correctly abstract shifts of arbitrary width as atoms instead of giving up.
 set_option trace.bv true in
-theorem shift_unit_6 {x y : BitVec 64} : (x >>> y) + y = y + (x >>> y) := by
+theorem shift_unit_6 {x y z : BitVec 16} : (x >>> y) >>> z = (x >>> z) >>> y := by
   bv_decide
 
 set_option trace.bv true in