[Agda] change in operator syntax

[Sergei Meshveliani]

On Thu, 2015-08-13 at 16:21 -0400, Wolfram Kahl wrote:
> 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!

Thank you.
 
Now, I add 
           infix 4 _Respects2_

But it cannot parse  _~_ and _≈_  in  Respects2←→Respects₂gen, where
_~_ and _≈_  are given as variable arguments in a function.
Then I remove their fixity changing them to  ~ and ≈,  and this is
parsed.

But generally:  if  _~_  is a variable argument in a function, then is
the programmer supposed to change it to  ~  and write (~ x y) instead of
(x ~ y)  everywhere in the body?

Regards,

------
Sergei