Alive build preexisting files (#119)

Do not yet add SSA.Projects.InstCombine.AliveAutoGenerated as it does not yet build.
opencompl · Oct 24, 2023 · 0d2e7ae · 0d2e7ae
1 parent 930f091
commit 0d2e7ae
Showing 1 changed file with 12 additions and 3 deletions.
diff --git a/SSA/Projects/InstCombine/Alive.lean b/SSA/Projects/InstCombine/Alive.lean
@@ -1,3 +1,12 @@
-/-
-  TODO: fix auto-generation script with new syntax
--/
+
+-- Auto generated alive statements
+-- import SSA.Projects.InstCombine.AliveAutoGenerated
+
+-- Pure math statements needed to proof alive statements
+import SSA.Projects.InstCombine.AliveStatements
+
+-- The semantics for the MLIR base dialect
+import SSA.Projects.InstCombine.Base
+
+-- An tactic for automatically proofing the alive math statements
+import SSA.Projects.InstCombine.TacticAuto