chore: clean up AliveStatements header (#600)

opencompl · Sep 8, 2024 · a9c1590 · a9c1590
1 parent 9379ce6
commit a9c1590
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 11 deletions.
diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean
@@ -1,16 +1,12 @@
-
 /-
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 import SSA.Projects.InstCombine.TacticAuto
-import SSA.Projects.InstCombine.ForStd
-import SSA.Projects.InstCombine.ForMathlib
 import SSA.Projects.InstCombine.LLVM.Semantics
 
 set_option linter.unreachableTactic false
 set_option linter.unusedTactic false
 
-
 theorem bitvec_AddSub_1043 :
     ∀ (e e_1 e_2 : LLVM.IntW w),
       LLVM.add (LLVM.add (LLVM.xor (LLVM.and e_2 e_1) e_1) (LLVM.const? 1)) e ⊑ LLVM.sub e (LLVM.or e_2 (LLVM.not e_1)) := by

diff --git a/SSA/Projects/InstCombine/update_alive_statements.py b/SSA/Projects/InstCombine/update_alive_statements.py
@@ -8,19 +8,14 @@
 import time
 import os
 
-alive_statements_preamble = """
-/-
+alive_statements_preamble = """/-
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 import SSA.Projects.InstCombine.TacticAuto
-import SSA.Projects.InstCombine.ForStd
-import SSA.Projects.InstCombine.ForMathlib
 import SSA.Projects.InstCombine.LLVM.Semantics
 
 set_option linter.unreachableTactic false
-set_option linter.unusedTactic false
-"""
-
+set_option linter.unusedTactic false"""
 
 def getProofs(lines: List[str]) -> Tuple[List[str], List[List[str]]]:
     """