summaryrefslogtreecommitdiff
path: root/Everything.agda
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2022-07-05 15:31:49 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2022-07-05 15:35:44 +0100
commit598d444c41db753e84dcaa920f484620cd375af7 (patch)
tree63d343a1abe5432063a1aaf2e33221d9721f82c0 /Everything.agda
parentb537d8e1bb0a06bc6e07b475eb32e726c2a115a6 (diff)
Define type.
Diffstat (limited to 'Everything.agda')
-rw-r--r--Everything.agda1
1 files changed, 1 insertions, 0 deletions
diff --git a/Everything.agda b/Everything.agda
index 0127e7e..a2b808f 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -2,3 +2,4 @@
module Everything where
import Data.BinOp
+import Data.Type