[Agda] First steps in agda

[Andreas Abel]

Hello Mathijs,

If you have a proof

   p : n + m == m + n

and you have

   v : Vector A (n + m)

then

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

see 
http://www.cse.chalmers.se/~nad/repos/lib/src/Relation/Binary/PropositionalEquality/Core.agda

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.

Cheers,
Andreas


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
http://www2.tcs.ifi.lmu.de/~abel/