[Agda] change in operator syntax

[Wolfram Kahl]

On Thu, Aug 13, 2015 at 11:06:31PM +0400, Sergei Meshveliani wrote:
> I am trying the  Development Agda of  August 13, 2015.
> 
> The attached code (25 nonempty lines) produces the report
> 
> -----------------
> Don't know how to parse _~_ Respects2 _≈_. Could mean any one of:
>   _Respects2_ _~_ _≈_
>   _Respects2_ _~_ _≈_
>   _Respects2_ _~_ _≈_
>   _Respects2_ _~_ _≈_
> Operators used in the grammar:
>   Respects2  (infix operator, unrelated)           [_Respects2_ 
>   ...
>   ...
> -----------------
> 
> What can be the matter about this?

As far as I know, operator parsing in the development version is
not yet settled, so it may change.

The main effect of the current state that I can see is that infix operators
without fixity declaration appear to be almost unusable.
>From the ``unrelated'' in the message above,
you see that Respects2 has no fixity declaration ---
if you use your own version of _Respects2_ , just add a fixity declaration.
If not, use the prefix application ``_Respects2_ _~_ _≈_''.
(In some cases, additional parentheses are required, too.)

(There seems to be no way to attach fixities to infix operators
 used as variables in pattern / as arguments.)


Hope this helps!


Wolfram