fix: add @[simp] attribute

leanprover · Feb 24, 2024 · b010052 · b010052
1 parent 7dbfbea
commit b010052
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -467,18 +467,18 @@ theorem getLsb_concat (x : BitVec w) (b : Bool) (i : Nat) :
 @[simp] theorem getLsb_concat_succ : (concat x b).getLsb (i + 1) = x.getLsb i := by
   simp [getLsb_concat]
 
-theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
+@[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
   ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ]
 
-theorem concat_or_concat (x y : BitVec w) (a b : Bool) :
+@[simp] theorem concat_or_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ||| (concat y b) = concat (x ||| y) (a || b) := by
   ext i; cases i using Fin.succRecOn <;> simp
 
-theorem concat_and_concat (x y : BitVec w) (a b : Bool) :
+@[simp] theorem concat_and_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) &&& (concat y b) = concat (x &&& y) (a && b) := by
   ext i; cases i using Fin.succRecOn <;> simp
 
-theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
+@[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (xor a b) := by
   ext i; cases i using Fin.succRecOn <;> simp