[Agda] change in operator syntax

[Nicolas Pouillard]

I second that. Please consider giving a default fixity.
Having a way to assign fixity of local names would be nice as well.

On 08/13/2015 10:21 PM, 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!
>
>
> Wolfram
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Best regards,
-- NP