[Agda] First steps in agda
mathijs at bluescreen303.nl
Wed Feb 13 21:03:02 CET 2013
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
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
Thanks for any help,
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda