mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-18 18:31:43 +03:00
32583d608d
and a small fix for the generation of method types which was okay for Blodwen, but not here
16 lines
305 B
Idris
16 lines
305 B
Idris
public export
|
|
interface Do (m : Type) where
|
|
Next : m -> Type
|
|
bind : (x : m) -> Next x
|
|
|
|
public export
|
|
Monad m => Do (m a) where
|
|
Next x = {b : Type} -> (a -> m b) -> m b
|
|
bind x k = x >>= k
|
|
|
|
foo : Maybe Int -> Maybe Int -> Maybe Int
|
|
foo x y
|
|
= bind x (\x' =>
|
|
bind y (\y' => Just (x' + y')))
|
|
|