chore: rebase on mul

leanprover · Jul 16, 2024 · 91ceedd · 91ceedd
1 parent 0e3d5f4
commit 91ceedd
Show file tree

Hide file tree

Showing 7 changed files with 5 additions and 7 deletions.
diff --git a/Eval/fail.txt b/Eval/fail.txt
@@ -1,17 +1,13 @@
-bitvec_160.lean
-bitvec_290__292.lean
 bitvec_AndOrXor_2443.lean
 bitvec_InstCombineShift__239.lean
 bitvec_InstCombineShift__279.lean
-bitvec_InstCombineShift__351.lean
 bitvec_InstCombineShift__422_1.lean
 bitvec_InstCombineShift__422_2.lean
 bitvec_InstCombineShift__440.lean
 bitvec_InstCombineShift__458.lean
 bitvec_InstCombineShift__476.lean
 bitvec_InstCombineShift__497.lean
 bitvec_InstCombineShift__582.lean
-bitvec_InstCombineShift__724.lean
 g2008h02h16hSDivOverflow2_proof.lean
 g2008h02h23hMulSub_proof.lean
 gadd2_proof.lean

diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Mul.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Mul.lean
@@ -63,7 +63,7 @@ theorem go_eq_eval_getLsb {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr
           rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := blastShiftLeftConst)]
           rw [hacc]
         . intros
-          simp only [blastShiftLeft_eq_eval_getLsb, BitVec.getLsb_shiftLeft]
+          simp only [blastShiftLeftConst_eq_eval_getLsb, BitVec.getLsb_shiftLeft]
           split
           . next hdiscr => simp [hdiscr]
           . next hidx hdiscr =>

diff --git a/Test/Eval.lean b/Test/Eval.lean
@@ -72,7 +72,6 @@ import Test.Eval.bitvec_AndOrXor_716
 import Test.Eval.bitvec_AndOrXor_794
 import Test.Eval.bitvec_AndOrXor_827
 import Test.Eval.bitvec_AndOrXor_887_2
-<<<<<<< HEAD
 import Test.Eval.g2004h02h23hShiftShiftOverflow_proof
 import Test.Eval.g2004h11h22hMissedhandhfold_proof
 import Test.Eval.g2008h07h08hSubAnd_proof
@@ -128,4 +127,7 @@ import Test.Eval.gunfoldhmaskedhmergehwithhconsthmaskhscalar_proof
 import Test.Eval.gxor2_proof
 import Test.Eval.gxorhofhor_proof
 import Test.Eval.bitvec_InstCombineShift__724
-import «Test.Eval.bitvec_InstCombineShift__497'''»
+import Test.Eval.bitvec_InstCombineShift__497_alt
+import Test.Eval.bitvec_160
+import Test.Eval.bitvec_290__292
+import Test.Eval.bitvec_InstCombineShift__351
diff --git a/Eval/bitvec_160.lean → Test/Eval/bitvec_160.lean b/Eval/bitvec_160.lean → Test/Eval/bitvec_160.lean
diff --git a/Eval/bitvec_290__292.lean → Test/Eval/bitvec_290__292.lean b/Eval/bitvec_290__292.lean → Test/Eval/bitvec_290__292.lean
diff --git a/Eval/bitvec_InstCombineShift__351.lean → Test/Eval/bitvec_InstCombineShift__351.lean b/Eval/bitvec_InstCombineShift__351.lean → Test/Eval/bitvec_InstCombineShift__351.lean
diff --git a/...Eval/bitvec_InstCombineShift__497'''.lean → ...val/bitvec_InstCombineShift__497_alt.lean b/...Eval/bitvec_InstCombineShift__497'''.lean → ...val/bitvec_InstCombineShift__497_alt.lean