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

[Wolfram Kahl]

On Fri, Mar 20, 2015 at 08:49:36AM +0100, Andreas Abel wrote:
> 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.

OK.


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

(It might be useful to point also to that on

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download

 and

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary

 --- is 2.4.2.3 the right branch to go with Agda maint-2.4.2 right now?

 I must admit that I haven't taken the time to learn git and github yet...

 How do I ``git clone'' Agda maint-2.4.2 directly?
 Under ``HTTPS clone URL'', I only find the repository home,
 and the links in ``You can clone with HTTPS or Subversion.''
 did not work for me, so I downloaded the ZIP file.

 How can I identify its precise version?
)


> 
> Concerning your problem below,

you mean ``(Setoid._≈_) S''?

> please submit a small test case to the 
> issue tracker (if you have not done so already).

Unfortunately it does not occur in complete isolation,
so I will have to experiment further, or strip one of the examples down.


Best,

Wolfram