diff options
Diffstat (limited to 'src/common/Optionmonad.v')
-rw-r--r-- | src/common/Optionmonad.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/common/Optionmonad.v b/src/common/Optionmonad.v index 4a80ff8..037dd83 100644 --- a/src/common/Optionmonad.v +++ b/src/common/Optionmonad.v @@ -43,13 +43,13 @@ Module Option <: Monad. | _ => None end. - Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B := + Definition bind {A B : Type} (g : A -> option B) (f : option A) : option B := match f with | Some a => g a | _ => None end. - Definition bind2 {A B C : Type} (f : mon (A * B)) (g : A -> B -> option C) : option C := + Definition bind2 {A B C : Type} (g : A -> B -> option C) (f : mon (A * B)) : option C := match f with | Some (a, b) => g a b | _ => None @@ -61,6 +61,12 @@ Module Option <: Monad. | Some a' => a' end. + #[global] Instance option_ret : MRet option := @ret. + #[global] Instance option_bind : MBind option := @bind. + #[global] Instance option_join : MJoin option := @join. + #[global] Instance option_map : FMap option := @map. + #[global] Instance option_omap : OMap option := @bind. + End Option. Module OptionExtra. |