[Agda] First steps in agda

[Mathijs Kwik]

Hi all,

I'm trying to figure out the basics of agda. I have a few years of haskell
experience, but lack a formal maths background. However, after some trying
and reading tutorials I managed to translate some proofs I found on
wikipedia into agda.

However, it's unclear to me how to use these proofs in other parts of my
program, where the typechecker complains and wants some proof.

Please have a look here:
https://gist.github.com/bluescreen303/4947548

How do I complete these 2 definitions?
Am I on the right track in general?
Or are there easier ways to accomplish things (apart from just using the
standard libraries)?
Furthermore, I noticed I've never used the . notation (as in suc .n), while
it's quite common in other code. Probably I'm doing something cumbersome to
avoid them?

Thanks for any help,
Mathijs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130213/7daa160e/attachment-0001.html