<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Since Coq has coersion, I use this functionality there. I assume that the use of coersion is not limited to the agda program text, but should also be presented in the interaction, namely in the proof window, the coersion functions would also be hidden. In this
situation, another request would probably follow immediately after coersion is implemented in Agda: add a switch to (temporarily) turn it off.
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Sometimes coersion can be confusing. I am not against it (since I use it), but I would say that this functionality could be very misleading if it overshoots too much, so the design of it is very important. I think the reason of this disagreement here is because
there is only one view of the program text, so we either have a very high level view but abstract, or a very low level view but too verbose. If we can have a hierarchy of views, which allows us to zoom in and out of mathematics/proofs/programs, I think coersion
can have way more value.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank"></a></b></span></span></font> </div>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Martin Escardo <m.escardo@cs.bham.ac.uk><br>
<b>Sent:</b> November 18, 2018 3:43 PM<br>
<b>To:</b> ulf.norell@gmail.com<br>
<b>Cc:</b> Agda mailing list<br>
<b>Subject:</b> Re: [Agda] I want implicit coercions in Agda</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt">
<div class="PlainText"><br>
<br>
On 18/11/2018 20:35, ulf.norell@gmail.com wrote:<br>
> On Sun, Nov 18, 2018 at 9:12 PM Martin Escardo <m.escardo@cs.bham.ac.uk <br>
> <<a href="mailto:m.escardo@cs.bham.ac.uk">mailto:m.escardo@cs.bham.ac.uk</a>>> wrote:<br>
> <br>
> <br>
> You will not solve the shortcomings of my mathematical style by<br>
> refusing<br>
> to implement implicit coercion in Agda.<br>
> <br>
> <br>
> I feel that the discussion has derailed a little at this point. The <br>
> issue isn't that some people<br>
> are stubbornly refusing to implement this <br>
<br>
This reply was not directed to the Agda developers, but instead to the <br>
people who ranted against these features.<br>
<br>
I will be happy to give a list of things for which implicit coercions <br>
are used by mathematicians, including those of my own Agda developments.<br>
<br>
Martin<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</body>
</html>