module Stdlib.Trait.Monad; import Stdlib.Data.Fixity open; import Stdlib.Trait.Applicative open; trait type Monad (m : Type -> Type) := mkMonad { {{applicative}} : Applicative m; builtin monad-bind bind : {A B : Type} -> m A -> (A -> m B) -> m B }; open Monad public; syntax operator >>= seq; >>= {A B} {f : Type -> Type} {{Monad f}} (x : f A) (g : A -> f B) : f B := bind x g; syntax operator >=> seq; >=> {A B C} {f : Type -> Type} {{Monad f}} (h : A -> f B) (g : B -> f C) (a : A) : f C := h a >>= g;