[Agda] infix ∸-mono ?

[Nils Anders Danielsson]

On 2017-05-04 13:51, Andrés Sicard-Ramírez wrote:
> Could you fix the accident, please.
>
> (I prefer a prefix version of  these functions)

And I prefer the infix version. I also suspect that you would break more
code by renaming _+-mono_ and _*-mono_ than by renaming ∸-mono.
Furthermore one could argue that it is better to leave the names as they
are, to avoid breaking code.

I no longer maintain the standard library, so I'm leaving this decision
to others.

-- 
/NAD