[Agda] Monads in std lib

[Daniel Peebles]

I've wondered about this before. What is the purpose of the
Raw<structure>/<structure> distinction in the standard library? I've
noticed it in the Algebra module too.

Thanks,
Dan

On Thu, Oct 1, 2009 at 9:19 AM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> On 2009-10-01 12:07, Jim Burton wrote:
>>
>> Tips?
>
> module MonadExample where
>
> open import Category.Monad
> open import Data.Maybe as Maybe
> open import Data.Nat
>
> maybeAdd : Maybe ℕ → Maybe ℕ → Maybe ℕ
> maybeAdd x y = x >>= λ x' →
>              y >>= λ y' →
>              return (x' + y')
>  where open RawMonad Maybe.monad
>
> --
> /NAD
>
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses, which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>