diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda
index ca45e0f..f267c4c 100644
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@@ -306,34 +306,4 @@ module WithProg (prog : Program) where
 
 
     -- Debugging code: print the resulting map.
-    open import Data.Fin using (suc; zero)
-    open import Data.Fin.Show using () renaming (show to showFin)
-    open import Data.Nat.Show using () renaming (show to showNat)
-    open import Data.String using (_++_)
-    open import Data.List using () renaming (length to lengthˡ)
-
     output = show signs
-
-
--- Debugging code: construct and run a program.
-open import Data.Vec using (Vec; _∷_; [])
-open import IO
-open import Level using (0ℓ)
-
-testCode : Vec Stmt _
-testCode =
-    ("zero" ← (# 0)) ∷
-    ("pos" ← ((` "zero") Expr.+ (# 1))) ∷
-    ("neg" ← ((` "zero") Expr.- (# 1))) ∷
-    ("unknown" ← ((` "pos") Expr.+ (` "neg"))) ∷
-    []
-
-testProgram : Program
-testProgram = record
-    { length = _
-    ; stmts = testCode
-    }
-
-open WithProg testProgram using (output)
-
-main = run {0ℓ} (putStrLn output)
diff --git a/Main.agda b/Main.agda
new file mode 100644
index 0000000..176bd5f
--- /dev/null
+++ b/Main.agda
@@ -0,0 +1,25 @@
+module Main where
+
+open import Language
+open import Analysis.Sign
+open import Data.Vec using (Vec; _∷_; [])
+open import IO
+open import Level using (0ℓ)
+
+testCode : Vec Stmt _
+testCode =
+    ("zero" ← (# 0)) ∷
+    ("pos" ← ((` "zero") Expr.+ (# 1))) ∷
+    ("neg" ← ((` "zero") Expr.- (# 1))) ∷
+    ("unknown" ← ((` "pos") Expr.+ (` "neg"))) ∷
+    []
+
+testProgram : Program
+testProgram = record
+    { length = _
+    ; stmts = testCode
+    }
+
+open WithProg testProgram using (output)
+
+main = run {0ℓ} (putStrLn output)