From b537d8e1bb0a06bc6e07b475eb32e726c2a115a6 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 5 Jul 2022 14:16:02 +0100 Subject: Define binary operations. --- Everything.agda | 4 ++++ src/Data/BinOp.agda | 6 ++++++ 2 files changed, 10 insertions(+) create mode 100644 Everything.agda create mode 100644 src/Data/BinOp.agda diff --git a/Everything.agda b/Everything.agda new file mode 100644 index 0000000..0127e7e --- /dev/null +++ b/Everything.agda @@ -0,0 +1,4 @@ +{-# OPTIONS --without-K --safe #-} +module Everything where + +import Data.BinOp 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 -- cgit v1.2.3