[Agda] lost fixity of ≈

[Andreas Källberg]

This is because you define a new operator named _≈_ and that new operator
has no fixity associated with it.

On Tue, 11 Dec 2018 at 14:53, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 11/12/2018 13.38, mechvel at scico.botik.ru wrote:
> > Is this a bug in Agda ?
>
> No.
>
> --
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181217/3e0401ee/attachment.html>