<div dir="ltr"><div><div><div><div><div><div><div>Hello Serge,<br><br></div>Now try to partially apply corresponding functions to the arguments you&#39;ve got after pattern matching.<br></div>I.e. Think what would you get <span style="font-family:monospace,monospace">hermes x y</span> if <span style="font-family:monospace,monospace">x</span> were <span style="font-family:monospace,monospace">zero</span>.<br></div>And the same for <span style="font-family:monospace,monospace">fold</span>.<br><br></div>You can use _ for the right hand side and compile your file to see what you need to place there.<br><br></div>Hope this will help.<br><br></div>Cheers,<br></div>Dmytro <br><div><div><div><div> <br></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">2015-04-04 23:19 GMT+03:00 Serge Leblanc <span dir="ltr">&lt;<a href="mailto:33dbqnxpy7if@gmail.com" target="_blank">33dbqnxpy7if@gmail.com</a>&gt;</span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  

    
  
  <div bgcolor="#FFFFFF" text="#000000">
    Hi, I&#39;m a Agda beginner and I try to proof that these two functions
    are similar :<br>
    <br>
    <small>module Hermes where<br>
        open import Data.Nat<br>
      <br>
      hermes : ℕ → ℕ → ℕ<br>
      hermes zero n = suc n<br>
      hermes (suc m) zero = hermes m (suc zero)<br>
      hermes (suc m) (suc n) = hermes m (hermes (suc m) n)<br>
      <br>
      hermes&#39; : ℕ → ℕ → ℕ<br>
      hermes&#39; m = fold suc (λ f p → fold 1 f (suc p)) m<br>
      <br>
      data _≡_ {A : Set} : A → A → Set where<br>
        refl : (a : A) → a ≡ a<br>
      <br>
      eq-suc : {n m : ℕ} → n ≡ m → suc n ≡ suc m<br>
      eq-suc (refl x) = refl (suc x)<br>
      <br>
      hermes≡hermes&#39; : (x y : ℕ) → hermes x y ≡ hermes&#39; x y<br>
      hermes≡hermes&#39; zero y = <br>
      hermes≡hermes&#39; (suc x) y = <br>
    </small><br>
    Could you help me?<br>
    <br>
    Sincerely,<span class="HOEnZb"><font color="#888888"><br>
    <div>-- <br>
      Serge Leblanc
      <hr>
      gpg --keyserver hkp://<a href="http://keyserver.ubuntu.com:11371" target="_blank">keyserver.ubuntu.com:11371</a> --recv-keys
      0x67B17A3F
      <br>
      Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
  </font></span></div>

<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>