Enable projects after move intrinsic asymptotics (#100)

* feat: re-enable InstCombine * chore: delete unused imports of WellTypedFramework * nit: bring back newline
opencompl · Oct 2, 2023 · 9b2df0c · 9b2df0c
1 parent a1f53f4
commit 9b2df0c
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 4 deletions.
diff --git a/SSA.lean b/SSA.lean
@@ -7,7 +7,7 @@ import SSA.Core.Framework
 -- ========
 
 -- Eventually, all projects must be imported.
--- import SSA.Projects.InstCombine.Alive
+import SSA.Projects.InstCombine.Alive
 -- import SSA.Projects.Tensor1D.Tensor1D
 -- import SSA.Projects.Tensor2D.Tensor2D
 

diff --git a/SSA/MLIRNatural.lean b/SSA/MLIRNatural.lean
@@ -1,4 +1,3 @@
--- import SSA.Core.WellTypedFramework
 import SSA.Projects.InstCombine.Tests
 import Cli
 
@@ -65,4 +64,5 @@ def mainCmd := `[Cli|
     ]
 
 def main (args : List String): IO UInt32 :=
-  mainCmd.validate args
+  mainCmd.validate args
+
diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
@@ -1,4 +1,3 @@
--- import SSA.Core.WellTypedFramework
 import SSA.Projects.InstCombine.Base
 import SSA.Projects.InstCombine.ForMathlib