[Agda] Monads in std lib

[Jim Burton]

Hi, the list once kindly explained to me how to use monadic instances for l=
ists, maybe etc.,
but the std lib has changed since then. The example below no longer works, =
as there is no
MaybeMonad declaration in Data.Monad. Looking at what has replaced it (in t=
he monad section of
Data.Maybe) I can't work out what I should be doing. Tips?

module MonadExample where

open import Category.Monad
open import Data.Maybe
open import Data.Nat

open module M =3D RawMonad MaybeMonad

maybeAdd : Maybe â„• -> Maybe â„• -> Maybe â„=
maybeAdd x y =3D x >>=3D \ x' ->
                y >>=3D \ y' ->
                return (x' + y')

Thanks,

Jim