[Agda] Agda beginner.

[Dmytro Starosud]

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.

Cheers,
Dmytro


2015-04-04 23:19 GMT+03:00 Serge Leblanc <33dbqnxpy7if at gmail.com>:

>  Hi, I'm a Agda beginner and I try to proof that these two functions are
> similar :
>
> module Hermes where
>   open import Data.Nat
>
> hermes : ℕ → ℕ → ℕ
> hermes zero n = suc n
> hermes (suc m) zero = hermes m (suc zero)
> hermes (suc m) (suc n) = hermes m (hermes (suc m) n)
>
> hermes' : ℕ → ℕ → ℕ
> hermes' m = fold suc (λ f p → fold 1 f (suc p)) m
>
> data _≡_ {A : Set} : A → A → Set where
>   refl : (a : A) → a ≡ a
>
> eq-suc : {n m : ℕ} → n ≡ m → suc n ≡ suc m
> eq-suc (refl x) = refl (suc x)
>
> hermes≡hermes' : (x y : ℕ) → hermes x y ≡ hermes' x y
> hermes≡hermes' zero y =
> hermes≡hermes' (suc x) y =
>
> Could you help me?
>
> Sincerely,
> --
> 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/20150405/946426a9/attachment.html