diff --git a/Makefile b/Makefile
index d412187..ab23ad5 100644
--- a/Makefile
+++ b/Makefile
@@ -1,16 +1,15 @@
-all: lib exe
+all: quox
+
+quox: exe
+	cp exe/build/exec/quox .
 
 .PHONY: lib
 lib:
 	idris2 --build quox.ipkg
 
-depends/quox: lib
-	mkdir -p depends
-	ln -sf ../build/ttc depends/quox
-
 .PHONY: exe
-exe: depends/quox
-	idris2 --build quox-exe.ipkg
+exe:
+	make -C exe exe
 
 .PHONY: test
 test:
@@ -19,4 +18,6 @@ test:
 .PHONY: clean
 clean:
 	rm -rf build depends
+	rm -f quox
+	make -C exe clean
 	make -C tests clean
diff --git a/Main.idr b/exe/Main.idr
similarity index 95%
rename from Main.idr
rename to exe/Main.idr
index 8fd706b..9544f88 100644
--- a/Main.idr
+++ b/exe/Main.idr
@@ -55,7 +55,7 @@ banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
 export
 tm : Term 1 2
 tm =
-  (Pi Zero One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
+  (Pi One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
     `DCloT` (K One ::: id))
     `CloT`  (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)
 
diff --git a/exe/Makefile b/exe/Makefile
new file mode 100644
index 0000000..19b9fb3
--- /dev/null
+++ b/exe/Makefile
@@ -0,0 +1,17 @@
+all: test
+
+.PHONY: lib
+lib:
+	make -C .. lib
+
+depends/quox: lib
+	mkdir -p depends
+	ln -sf ../../build/ttc depends/quox
+
+.PHONY: test
+exe: depends/quox
+	idris2 --build quox-exe.ipkg
+
+.PHONY: clean
+clean:
+	rm -rf build depends
diff --git a/quox-exe.ipkg b/exe/quox-exe.ipkg
similarity index 100%
rename from quox-exe.ipkg
rename to exe/quox-exe.ipkg