diff options
Diffstat (limited to 'src/common/Errormonad.v')
-rw-r--r-- | src/common/Errormonad.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/common/Errormonad.v b/src/common/Errormonad.v index 09c5c1c..201a101 100644 --- a/src/common/Errormonad.v +++ b/src/common/Errormonad.v @@ -26,13 +26,13 @@ Module ErrorMonad <: Monad. | Error m => Error m end. - Definition bind {A B : Type} (f : mon A) (g : A -> mon B) : mon B := + Definition bind {A B : Type} (g : A -> mon B) (f : mon A) : mon B := match f with | OK a => g a | Error m => Error m end. - Definition bind2 {A B C : Type} (f : mon (A * B)) (g : A -> B -> mon C) : mon C := + Definition bind2 {A B C : Type} (g : A -> B -> mon C) (f : mon (A * B)) : mon C := match f with | OK (a, b) => g a b | Error m => Error m @@ -44,6 +44,11 @@ Module ErrorMonad <: Monad. | OK a' => a' end. + #[global] Instance error_ret : MRet res := @ret. + #[global] Instance error_bind : MBind res := @bind. + #[global] Instance error_join : MJoin res := @join. + #[global] Instance error_map : FMap res := @map. + End ErrorMonad. Module ErrorMonadExtra := MonadExtra(ErrorMonad). |