[Agda] lost fixity of ≈

[Sergei Meshveliani]

On Mon, 2018-12-17 at 09:48 +0100, Andreas Källberg wrote:
> This is because you define a new operator named _≈_ and that new
> operator has no fixity associated with it.


Thank you. I see now.
I occurs that the effect of
                         open Foo foo using (_≈_)
and                      _≈_ = Foo._≈_ foo
is different.


> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda