[Agda] Some newbie questions

[J.Burton at brighton.ac.uk]

At Fri, 21 Nov 2008 12:38:22 -0500,
Darin Morrison wrote:
> 
> On Nov 21, 2008, at 11:58 AM, J.Burton at brighton.ac.uk wrote:
> 
> > Hi, how do I use monad instances? If I import Data.List or Data.Maybe
> > then return >>= are apparently not in scope.
> >
> 
> Here's a short example:

Thanks!

> 
> module MonadExample where
> 
> open import Category.Monad
> open import Data.Maybe
> open import Data.Nat
> 
> open module M = RawMonad MaybeMonad
> 
> maybeAdd : Maybe ? -> Maybe ? -> Maybe ?
> maybeAdd x y = x >>= \ x' ->
>                 y >>= \ y' ->
>                 return (x' + y')
> 
> 
> 
> The key is that you need to bring the fields from the MaybeMonad  
> record in the Data.Maybe module into scope.  This is explained a bit  
> more here:
> 
> http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=ReferenceManual.Records
> 
[...]
> 
> I'm pretty sure you can't pattern match with lambdas.
> 

Oh, that's a pity.

Jim

> Regards,
> Darin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081121/9895170f/attachment.html