diff options
Diffstat (limited to 'transfer/lib/maybe.tr')
| -rw-r--r-- | transfer/lib/maybe.tr | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/transfer/lib/maybe.tr b/transfer/lib/maybe.tr index 02d7fe56d..2b7beee9a 100644 --- a/transfer/lib/maybe.tr +++ b/transfer/lib/maybe.tr @@ -1,3 +1,5 @@ +import prelude + data Maybe : Type -> Type where Nothing : (A : Type) -> Maybe A Just : (A : Type) -> A -> Maybe A @@ -8,4 +10,15 @@ 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 +maybe _ _ _ f (Just x) = f x + +-- Instances: + +monad_Maybe : Monad Maybe +monad_Maybe = + rec return = Just + bind = \A -> \B -> \m -> \k -> + case m of + Nothing _ -> Nothing B + Just _ x -> k x + |