summaryrefslogtreecommitdiff
path: root/Everything.agda
diff options
context:
space:
mode:
authorHelmut Grohne <grohne@cs.uni-bonn.de>2014-01-30 08:07:29 +0100
committerHelmut Grohne <grohne@cs.uni-bonn.de>2014-01-30 08:07:29 +0100
commit26e2fea33aae257440e5571fb3f7e784938403e0 (patch)
treee2c6d087dbb7e9476cf2e613125840923b3f139a /Everything.agda
parentb0eb7ada208d33eb82ec27cb7d40b9fa59646c92 (diff)
downloadbidiragda-26e2fea33aae257440e5571fb3f7e784938403e0.tar.gz
simplify compilation of the whole source
Diffstat (limited to 'Everything.agda')
-rw-r--r--Everything.agda11
1 files changed, 11 insertions, 0 deletions
diff --git a/Everything.agda b/Everything.agda
new file mode 100644
index 0000000..76beef6
--- /dev/null
+++ b/Everything.agda
@@ -0,0 +1,11 @@
+-- The sole purpose of this module is to ease compilation of everything.
+module Everything where
+
+import Generic
+import FinMap
+import CheckInsert
+import FreeTheorems
+import BFF
+import Bidir
+import LiftGet
+import Precond