[Agda] "with" notation?

[Pierre-Evariste Dagand]

> I probably should have asked how to write the monadic notation for
> passing around objects of the Maybe type.

As far as I know (that is, very little), the standard library defines
Data.Maybe as a Category.Monad. Looking at Category.Monad.Indexed, you
can see that you get the usual bind and return operators (>>=, return)
and their little friends.

I don't know if there is something similar to a "do-notation", tho.


Hope this help,

-- 
Pierre-Evariste