[Agda] Some newbie questions

J.Burton at brighton.ac.uk J.Burton at brighton.ac.uk
Fri Nov 21 17:58:35 CET 2008


Hi, how do I use monad instances? If I import Data.List or Data.Maybe
then return >>= are apparently not in scope.

I'm confused about lambdas too...can I pattern match over their
arguments? Here is a simplified version of something I was trying to
do:

data T ? : Set where
S : ? -> T ?

h : T ? -> ?
h = \ S i -> i   

gives the error "? != (i : _26 S) -> _27 S i of type Set
when checking that the expression \i -> i has type ?"

Adding brackets to get `\ (S i) -> i' doesn't help: "Parse error
)<ERROR>
 -> i" 

Thanks,

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


More information about the Agda mailing list