Added transfer Maybe module.
This commit is contained in:
1 parent
f2e0c40f5b
commit
71b77a5481
1 file changed
+11
@@ -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
|
||||
Reference in new issue
Block a user