Added transfer Maybe module.

1 files changed, 11 insertions, 0 deletions

diff --git a/transfer/examples/maybe.tr b/transfer/examples/maybe.tr
new file mode 100644
index 000000000..02d7fe56d
--- /dev/null
+++ b/transfer/examples/maybe.tr
@@ -0,0 +1,11 @@
+data Maybe : Type -> Type where
+	Nothing : (A : Type) -> Maybe A
+	Just : (A : Type) -> A -> Maybe A
+
+fromMaybe : (A : Type) -> A -> Maybe A -> A
+fromMaybe _ x Nothing = x
+fromMaybe _ _ (Just x) = x
+
+maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A
+maybe _ _ x _ Nothing = x
+maybe _ _ _ f (Just x) = f x
\ No newline at end of file