Skip to content
Snippets Groups Projects
Commit 1534af50 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Ralf Jung
Browse files

Also use + for monad.

parent 3aaeed9c
No related branches found
No related tags found
No related merge requests found
......@@ -1144,27 +1144,27 @@ class with the monad laws). *)
Class MRet (M : Type Type) := mret: {A}, A M A.
Global Arguments mret {_ _ _} _ : assert.
Global Instance: Params (@mret) 3 := {}.
Global Hint Mode MRet ! : typeclass_instances.
Global Hint Mode MRet + : typeclass_instances.
Class MBind (M : Type Type) := mbind : {A B}, (A M B) M A M B.
Global Arguments mbind {_ _ _ _} _ !_ / : assert.
Global Instance: Params (@mbind) 4 := {}.
Global Hint Mode MBind ! : typeclass_instances.
Global Hint Mode MBind + : typeclass_instances.
Class MJoin (M : Type Type) := mjoin: {A}, M (M A) M A.
Global Arguments mjoin {_ _ _} !_ / : assert.
Global Instance: Params (@mjoin) 3 := {}.
Global Hint Mode MJoin ! : typeclass_instances.
Global Hint Mode MJoin + : typeclass_instances.
Class FMap (M : Type Type) := fmap : {A B}, (A B) M A M B.
Global Arguments fmap {_ _ _ _} _ !_ / : assert.
Global Instance: Params (@fmap) 4 := {}.
Global Hint Mode FMap ! : typeclass_instances.
Global Hint Mode FMap + : typeclass_instances.
Class OMap (M : Type Type) := omap: {A B}, (A option B) M A M B.
Global Arguments omap {_ _ _ _} _ !_ / : assert.
Global Instance: Params (@omap) 4 := {}.
Global Hint Mode OMap ! : typeclass_instances.
Global Hint Mode OMap + : typeclass_instances.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment