Fix build

opencompl · Sep 28, 2024 · 4fbba5e · 4fbba5e
1 parent 919a385
commit 4fbba5e
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -508,6 +508,8 @@ theorem not_sshiftRight_not {x : BitVec w} {n : Nat} :
     ~~~((~~~x).sshiftRight n) = x.sshiftRight n := by
   simp [not_sshiftRight]
 
+attribute [simp] shiftLeft_ushiftRight
+
 theorem ofInt_neg_one : BitVec.ofInt w (-1) = -1#w := by
   simp only [Int.reduceNeg, toNat_eq, toNat_ofInt, Nat.cast_pow, Nat.cast_ofNat, toNat_neg,
     toNat_ofNat]