[Agda] I want implicit coercions in Agda

[Ulf Norell]

On Sun, Nov 18, 2018 at 9:12 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

>
> You will not solve the shortcomings of my mathematical style by refusing
> to implement implicit coercion in Agda.
>

I feel that the discussion has derailed a little at this point. The issue
isn't that some people
are stubbornly refusing to implement this one simple thing that would make
life easier for
the practising mathematician. The problem is that implicit coercions are
very difficult to get
right. To move this discussion forward I suggest that you give some of the
following:

- concrete examples of implicit coercions that you'd like to see
- a rough sketch of how they are to be solved
- references to the proof assistants that (in your opinion) have gotten
implicit coercions right
- some notes on why instance arguments are not a good replacement for
implicit coercions

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181118/9a9dfef3/attachment.html>