From 16d547a3807a8c51fcac6270c76540f6e7b89cf2 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 30 Jun 2023 17:08:06 +0100
Subject: Initial commit.

---
 src/Data/Maybe/Properties.idr | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 src/Data/Maybe/Properties.idr

(limited to 'src/Data/Maybe/Properties.idr')

diff --git a/src/Data/Maybe/Properties.idr b/src/Data/Maybe/Properties.idr
new file mode 100644
index 0000000..f00b79f
--- /dev/null
+++ b/src/Data/Maybe/Properties.idr
@@ -0,0 +1,6 @@
+module Data.Maybe.Properties
+
+export
+mapFusion : (s : Maybe a) -> (f . g) <$> s = f <$> [| g s |]
+mapFusion Nothing = Refl
+mapFusion (Just x) = Refl
-- 
cgit v1.2.3