[Agda] First steps in agda

Andreas Abel andreas.abel at ifi.lmu.de
Thu Feb 14 14:15:22 CET 2013

Hello Mathijs,

If you have a proof

   p : n + m == m + n

and you have

   v : Vector A (n + m)


   subst (Vector A) p v : Vector A (m + n)


However, it is advisable that append for vectors and plus have the same 
argument ordering, so maybe you want to define + by cases on the first 
argument and not the second.


On 13.02.13 9:03 PM, Mathijs Kwik wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list