summaryrefslogtreecommitdiff
path: root/src/Data/Maybe/Properties.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Maybe/Properties.idr')
-rw-r--r--src/Data/Maybe/Properties.idr6
1 files changed, 6 insertions, 0 deletions
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