<div dir="ltr">On Sun, Nov 18, 2018 at 9:12 PM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>You will not solve the shortcomings of my mathematical style by refusing <br>
to implement implicit coercion in Agda.<br></blockquote><div><br></div><div>I feel that the discussion has derailed a little at this point. The issue isn't that some people</div><div>are stubbornly refusing to implement this one simple thing that would make life easier for</div><div>the practising mathematician. The problem is that implicit coercions are very difficult to get</div><div>right. To move this discussion forward I suggest that you give some of the following:</div><div><br></div><div>- concrete examples of implicit coercions that you'd like to see</div><div>- a rough sketch of how they are to be solved</div><div>- references to the proof assistants that (in your opinion) have gotten implicit coercions right</div><div>- some notes on why instance arguments are not a good replacement for implicit coercions</div><div><br></div><div>/ Ulf</div><div><br></div></div></div>