summaryrefslogtreecommitdiff
path: root/src/index.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/index.agda')
-rw-r--r--src/index.agda9
1 files changed, 0 insertions, 9 deletions
diff --git a/src/index.agda b/src/index.agda
deleted file mode 100644
index 4acb132..0000000
--- a/src/index.agda
+++ /dev/null
@@ -1,9 +0,0 @@
-module index where
-
--- You probably want to start with this module:
-import README
-
--- For a brief presentation of every single module, head over to
-import Everything
-
--- Otherwise, here is an exhaustive, stern list of all the available modules: