use_simp_llvm_option set

SSA/Projects/InstCombine/LLVM/Semantics.lean

@@ -21,7 +21,7 @@ The ‘and’ instruction returns the bitwise logical and of its two operands.
 def and? {w : Nat} (x y : BitVec w) : IntW w :=
   pure <| x &&& y
 
-@[simp]
+@[simp_llvm_option]
 theorem and?_eq : LLVM.and? a b  = .some (BitVec.and a b) := rfl
 
 @[simp_llvm_option]
@@ -38,7 +38,7 @@ operands.
 def or? {w : Nat} (x y : BitVec w) : IntW w :=
   pure <| x ||| y
 
-@[simp]
+@[simp_llvm_option]
 theorem or?_eq : LLVM.or? a b  = .some (BitVec.or a b) := rfl
 
 @[simp_llvm_option]
@@ -56,7 +56,7 @@ is the “~” operator in C.
 def xor? {w : Nat} (x y : BitVec w) : IntW w :=
   pure <| x ^^^ y
 
-@[simp]
+@[simp_llvm_option]
 theorem xor?_eq : LLVM.xor? a b  = .some (BitVec.xor a b) := rfl
 
 @[simp_llvm_option]
@@ -74,7 +74,7 @@ Because LLVM integers use a two’s complement representation, this instruction
 def add? {w : Nat} (x y : BitVec w) : IntW w :=
   pure <| x + y
 
-@[simp]
+@[simp_llvm_option]
 theorem add?_eq : LLVM.add? a b  = .some (BitVec.add a b) := rfl
 
 @[simp_llvm_option]
@@ -92,7 +92,7 @@ Because LLVM integers use a two’s complement representation, this instruction
 def sub? {w : Nat} (x y : BitVec w) : IntW w :=
   pure <| x - y
 
-@[simp]
+@[simp_llvm_option]
 theorem sub?_eq : LLVM.sub? a b  = .some (BitVec.sub a b) := rfl
 
 @[simp_llvm_option]
@@ -116,7 +116,7 @@ sign-extended or zero-extended as appropriate to the width of the full product.
 def mul? {w : Nat} (x y : BitVec w) : IntW w :=
   pure <| x * y
 
-@[simp]
+@[simp_llvm_option]
 theorem mul?_eq : LLVM.mul? a b  = .some (BitVec.mul a b) := rfl
 
 @[simp_llvm_option]
@@ -428,14 +428,14 @@ TODO: double-check that truncating works the same as MLIR (signedness, overflow,
 def const? (i : Int): IntW w :=
   pure <| BitVec.ofInt w i
 
-@[simp]
+@[simp_llvm_option]
 theorem LLVM.const?_eq : LLVM.const? i = .some (BitVec.ofInt w i) := rfl
 
 @[simp_llvm]
 def not? {w : Nat} (x : BitVec w) : IntW w := do
   pure (~~~x)
 
-@[simp]
+@[simp_llvm_option]
 theorem LLVM.not?_eq : LLVM.not? a = .some (BitVec.not a) := rfl
 
 @[simp_llvm_option]
@@ -447,7 +447,7 @@ def not {w : Nat} (x : IntW w) : IntW w := do
 def neg? {w : Nat} (x : BitVec w) : IntW w := do
   pure <| (-.) x
 
-@[simp]
+@[simp_llvm_option]
 theorem LLVM.neg?_eq : LLVM.neg? a = .some (BitVec.neg a) := rfl
 
 @[simp_llvm_option]