<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
Dear Philippe,<br>
<br>
These Agda exercise sessions - mostly by Jesper Cockx - may be of
interest to you:<br>
<a class="moz-txt-link-freetext" href="https://github.com/anuyts/agda-sessions">https://github.com/anuyts/agda-sessions</a><br>
<br>
To answer your question:<br>
<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>
<br>
Best regards,<br>
Andreas<br>
<br>
<div class="moz-cite-prefix">On 18/04/2020 17:32, Philippe de
Rochambeau wrote:<br>
</div>
<blockquote type="cite"
cite="mid:5D08F574-4173-482C-B79D-95A4BDA7A89D@free.fr">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
s/« which the user can then apply » /« letting the use apply
them »/<br class="">
<div><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>
<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>
</body>
</html>