[Agda] First steps in agda

Mathijs Kwik mathijs at bluescreen303.nl
Wed Feb 13 21:03:02 CET 2013

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:

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,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130213/7daa160e/attachment-0001.html

More information about the Agda mailing list