From 1534af50dfb6c9f23a205fb9cb8f2ada079ad3f0 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sat, 3 Dec 2022 19:43:26 +0100 Subject: [PATCH] Also use + for monad. --- stdpp/base.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/stdpp/base.v b/stdpp/base.v index 9b98d728..f9daa200 100644 --- a/stdpp/base.v +++ b/stdpp/base.v @@ -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. -- GitLab