Updated Everything.agda and Makefile

flupe · Mar 2, 2022 · de72c83 · de72c83
1 parent 6207db2
commit de72c83
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 8 deletions.
diff --git a/Everything.agda b/Everything.agda
@@ -14,7 +14,6 @@ import Generics.Mu
 import Generics.Mu.All
 import Generics.Mu.Elim
 import Generics.Mu.Fold
-import Generics.Mu.Conversion
 
 import Generics.Constructions.Case
 import Generics.Constructions.Cong
@@ -23,12 +22,7 @@ import Generics.Constructions.Elim
 import Generics.Constructions.Fold
 import Generics.Constructions.Mu
 import Generics.Constructions.Recursion
+import Generics.Constructions.NoConfusion
 import Generics.Constructions.Show
 
 import Generics
-
--- Work In Progress
----------------------------------
-
--- import Generics.Mu.NoConfusion
--- import Generics.Constructions.Injective
diff --git a/Makefile b/Makefile
@@ -1,7 +1,10 @@
 AGDA ?= agda
 .PHONY: listings clean
 
-default: listings
+default: everything
+
+everything:
+	$(AGDA) -i. -isrc Everything.agda
 
 listings:
 	$(AGDA) -i. -isrc --html README.agda -v0