[Agda] I want implicit coercions in Agda

[Martin Escardo]

On 17/11/2018 10:29, mechvel at botik.ru wrote:

> Generally, we need to respect mathematical style.
> It is based on experience of many centuries.
> Most of the mathematical community really understands which book is
> easier to read.
> I tend to trust this approach more.

Exactly. I fully agree.

If implicit coercions are ever implemented, I propose that the emacs 
mode and the html rendering highlight the implicitly coerced things with 
a different color so that the reader can see that there is a coercion 
being applied.

Martin