[Agda] change in operator syntax

[Andrea Vezzosi]

If you want to try the devel version of Agda without having to change
too much about fixities you can pull from the freshly made
def-fixities branch.

https://github.com/agda/agda/tree/def-fixities

I haven't merged this in the master because it breaks some of the test
suite at the moment.
However the general plan is to have default fixities back.

Cheers,
Andrea

On Fri, Aug 14, 2015 at 11:22 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> 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
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda