summaryrefslogtreecommitdiff
path: root/src/Data/BinOp.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/BinOp.agda')
-rw-r--r--src/Data/BinOp.agda6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Data/BinOp.agda b/src/Data/BinOp.agda
new file mode 100644
index 0000000..610c68d
--- /dev/null
+++ b/src/Data/BinOp.agda
@@ -0,0 +1,6 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.BinOp where
+
+data BinOp : Set where
+ Function : BinOp