<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Very enlightening.<div class=""><br class=""></div><div class="">Thank you, Andreas.<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">Le 18 avr. 2020 à 17:37, Andreas Nuyts <<a href="mailto:andreas.nuyts@kuleuven.be" class="">andreas.nuyts@kuleuven.be</a>> a écrit :</div><br class="Apple-interchange-newline"><div class="">
  
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class="">
  
  <div class="">
    Dear Philippe,<br class="">
    <br class="">
    These Agda exercise sessions - mostly by Jesper Cockx - may be of
    interest to you:<br class="">
    <a class="moz-txt-link-freetext" href="https://github.com/anuyts/agda-sessions">https://github.com/anuyts/agda-sessions</a><br class="">
    <br class="">
    To answer your question:<br class="">
    <span style="font-variant-ligatures: no-common-ligatures" class="">tauto₁</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color:
      #535353" class="">=</span><span style="font-variant-ligatures:
      no-common-ligatures;" class=""> </span>\ A B C g f a -> g a (f
    a)<br class="">
    <br class="">
    Best regards,<br class="">
    Andreas<br class="">
    <br class="">
    <div class="moz-cite-prefix">On 18/04/2020 17:32, Philippe de
      Rochambeau wrote:<br class="">
    </div>
    <blockquote type="cite" cite="mid:5D08F574-4173-482C-B79D-95A4BDA7A89D@free.fr" class="">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class="">
      s/« which the user can then apply » /«  letting the use apply
      them »/<br class="">
      <div class=""><br class="">
        <blockquote type="cite" class="">
          <div class="">Le 18 avr. 2020 à 17:30, Philippe de Rochambeau
            <<a href="mailto:phiroc@free.fr" class="" moz-do-not-send="true">phiroc@free.fr</a>> a écrit :</div>
          <br class="Apple-interchange-newline">
          <div class="">
            <div style="word-wrap: break-word; -webkit-nbsp-mode: space;
              line-break: after-white-space;" class="">
              <div class=""><br class="">
              </div>
              <div class="">Hello,</div>
              <div class=""><br class="">
              </div>
              <div class="">I am attempting to translate a Coq proof
                into Agda, for learning purposes (cf. <a href="https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf" class="" moz-do-not-send="true">https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf</a>,
                p. 9):</div>
              <div class=""><br class="">
              </div>
              <div class="">
                <div style="margin: 0px; font-stretch: normal;
                  line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures;
                    color: #4500ff" class="">tauto₁</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">∀</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">A B C </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #4500ff" class="">Set</span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">A </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> B </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> C</span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">A </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> B</span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> A </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> C</span></div>
                <div style="margin: 0px; font-stretch: normal;
                  line-height: normal; font-family: Menlo; color:
                  rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">tauto₁</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures: no-common-ligatures;
                    color: #343434; background-color: #a2ff9f" class="">{
                    }</span><span style="font-variant-ligatures:
                    no-common-ligatures; background-color: rgb(162, 255,
                    159);" class="">0</span></div>
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal; font-family: Menlo; color: rgb(69,
                0, 255);" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class="">Here’s how Coq introduces
                hypotheses, letting the use apply them.</div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal; font-family: Menlo; color: rgb(69,
                0, 255);" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  236.23px; top: 794.986px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.849653);" class="">Coq < apply H’.</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  236.23px; top: 814.911px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);" class="">1 </span><span style="left: 236.23px; top:
                  814.911px; font-size: 16.6043px; font-family:
                  monospace; transform: scaleX(0.999592);" class="">subgoal</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 854.761px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);" class="">A : Prop</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 874.687px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);" class="">B : Prop</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 894.612px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);" class="">C : Prop</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 914.537px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);" class="">H : A -> B -> C</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 934.462px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);" class="">H’ : A -> B</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 954.387px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);" class="">HA : A</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 974.312px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);" class="">============================</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  266.118px; top: 994.239px; font-size: 16.6043px;
                  font-family: monospace;" class="">A</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class="">How do you do the same
                thing in Agda?</div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class="">Cheers,</div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class="">Philippe</div>
            </div>
            _______________________________________________<br class="">
            Agda mailing list<br class="">
            <a href="mailto:Agda@lists.chalmers.se" class="" moz-do-not-send="true">Agda@lists.chalmers.se</a><br class="">
            <a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
          </div>
        </blockquote>
      </div>
      <br class="">
      <br class="">
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br class="">
  </div>

</div></blockquote></div><br class=""></div></body></html>