<div dir="ltr"><div><div>As Andrés said, I unfortunately cannot test DoCon-A-0.03 with my new unifier because I get a parse error at source/Int/Integer1.agda:418,11-422,15. Do you have a version that is compatible with the current Agda master?<br><br></div>regards,<br></div>Jesper<br><div><div><div><div><br></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Dec 15, 2015 at 2:32 PM, Andrés Sicard-Ramírez <span dir="ltr"><<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 14 December 2015 at 16:10, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br>
> You can use the test of DoCon-A-0.03:<br>
><br>
> <a href="http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/" rel="noreferrer" target="_blank">http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/</a><br>
<br>
</span>DoCon-A-0.03 doesn't type-check with the development version (i.e. the<br>
master branch), so it's not possible to test Jesper's new unifier.<br>
<span class=""><br>
><br>
> I am not sure that I would try it now, because it is very difficult to<br>
> advance the project when trying different tool versions.<br>
><br>
<br>
</span>It's not difficult to test Jesper's new unifier. By running<br>
<span class=""><br>
$ git clone <a href="https://github.com/jespercockx/agda.git" rel="noreferrer" target="_blank">https://github.com/jespercockx/agda.git</a> agda-unification<br>
$ cd agda-unification<br>
$ git checkout --track origin/unification<br>
$ make install-bin<br>
<br>
</span>you get a version of Agda including Jesper' new unifier (Agda 2.5).<br>
After type-checking you code, you remove the agda-unification<br>
directory and you re-install Agda from your current directory.<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
--<br>
Andrés<br>
</font></span></blockquote></div><br></div>