From 4fbba5e4c93149f0f8a456316170ecbee1c0dcad Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 28 Sep 2024 07:38:08 +0100
Subject: [PATCH] Fix build

---
 SSA/Projects/InstCombine/ForLean.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 2e4ad3917..93c94665f 100644
--- 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]