<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>