[Agda-dev] Qualified full operator name now needs parentheses?

[Andreas Abel]

Wolfram,

things are in the flux with the parser on the master version.  The 
current state is not what we will release, as is it not satisfactory.

To get bugfixes, I suggest to use the maint-2.4.2 branch.

Concerning your problem below, please submit a small test case to the 
issue tracker (if you have not done so already).

Best,
Andreas

On 20.03.2015 01:45, Wolfram Kahl wrote:
> I'm still fighting my way through updating my developments
> to a recent development version, and get errors that I consider as quite surprising:
>
>   | Could not parse the application Setoid._≈_ S
>   | (the treatment of operators has changed, so code that used to parse
>   | may have to be changed)
>   | when scope checking Setoid._≈_ S
>
> Changing this to
>
>    (Setoid._≈_) S
>
> makes it parse --- is this requirement for parentheses intentional?
> I don't find this mentioned in doc/release-notes/2-4-4.txt.
>
>
> Related: Is there a way to declare fixity for operators that are
> module parameters?
> (Or even for function arguments?)
>
>
> Also quite surprising are error messages resulting from
>
>   | * If an overloaded operator is in scope with several distinct
>   |   fixities, then several instances of this operator will be included
>   |   in the operator grammar, possibly leading to ambiguity.
>
> because the error message happily shows the two parses
> as identical strings.
> (I am not even sure that the different infix constructors had different fixity ---
>   I'll have to check that when I encounter it again.)
>
>
> Wolfram
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/