[Agda-dev] Qualified full operator name now needs parentheses?
Wolfram Kahl
kahl at cas.mcmaster.ca
Fri Mar 20 15:17:47 CET 2015
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
More information about the Agda-dev
mailing list