[Agda] Agda beginner.

[Dmytro Starosud]

If you get stuck using pattern matching on first argument try to split
using another...

Cheers,
Dmytro

P.S. actually theorem proving is undecidable in general:-D so you shouldn't
except to get all the knowledge required for this in one go (and even in
many;)).
I would suggest you first just try to repeat some existing profs to become
familiar with this process.





2015-04-06 12:25 GMT+03:00 Serge Leblanc <33dbqnxpy7if at gmail.com>:

>  Thanks Dmytro, is trivial when x = 0, but I have more difficulty when x
> > 0.
>
> hermes≡hermes' : (x y : ℕ) → hermes x y ≡ hermes' x y
> hermes≡hermes' zero y = refl (suc y)
> hermes≡hermes' (suc x) y = { }0   {- ?0 : hermes (suc x) y ≡ hermes' (suc
> x) y -}
>
>
> On 2015-04-05 14:06, Dmytro Starosud wrote:
>
>   Hello Serge,
>
>  Now try to partially apply corresponding functions to the arguments
> you've got after pattern matching.
>  I.e. Think what would you get hermes x y if x were zero.
>  And the same for fold.
>
>  You can use _ for the right hand side and compile your file to see what
> you need to place there.
>
>  Hope this will help.
>
>
>
> --
> Serge Leblanc
> ------------------------------
> gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150406/cbce1c88/attachment.html