chore: disable unreachable tactic warning in AliveStatements (#302)

opencompl · May 13, 2024 · 8ce2bb6 · 8ce2bb6
1 parent 146c822
commit 8ce2bb6
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean
@@ -12,6 +12,8 @@ import Mathlib.Data.BitVec.Lemmas
 open LLVM
 open BitVec
 
+set_option linter.unreachableTactic false
+
 
 theorem bitvec_AddSub_1043 :
     ∀ (e e_1 e_2 : LLVM.IntW w),

diff --git a/SSA/Projects/InstCombine/update_alive_statements.py b/SSA/Projects/InstCombine/update_alive_statements.py
@@ -21,6 +21,8 @@
 
 open LLVM
 open BitVec
+
+set_option linter.unreachableTactic false
 """
-Original file line number
+Diff line change
@@ Expand Up / @@ -21,6 +21,8 @@ @@
     open LLVM
     open BitVec
+    set_option linter.unreachableTactic false
     """
@@ Expand Down @@