diff options
Diffstat (limited to 'src/common/Statemonad.v')
| -rw-r--r-- | src/common/Statemonad.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v index 16dcbbf..c667fd9 100644 --- a/src/common/Statemonad.v +++ b/src/common/Statemonad.v @@ -42,7 +42,7 @@ Module Statemonad(S : State) <: Monad. Definition ret {A: Type} (x: A) : mon A := fun (s : S.st) => OK x s (S.st_refl s). - 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 := fun (s : S.st) => match f s with | Error msg => Error msg @@ -53,8 +53,8 @@ Module Statemonad(S : State) <: Monad. end end. - Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C := - bind f (fun xy => g (fst xy) (snd xy)). + Definition bind2 {A B C: Type} (g: A -> B -> mon C) (f: mon (A * B)) : mon C := + bind (fun xy => g (fst xy) (snd xy)) (f: mon (A * B)). Definition handle_error {A: Type} (f g: mon A) : mon A := fun (s : S.st) => @@ -76,4 +76,7 @@ Module Statemonad(S : State) <: Monad. | Error err => Errors.Error err end. + #[global] Instance statemonad_ret : MRet mon := @ret. + #[global] Instance statemonad_bind : MBind mon := @bind. + End Statemonad. |