[Agda-dev] A new unifier for case splitting

Jesper Cockx Jesper at sikanda.be
Wed Jan 6 14:15:33 CET 2016


Thank you very much to Andrés and Sergei for testing my code. Since I got
no further response and all immediate problems are solved, I have merged my
pull request into master. You can read the patch notes at
https://github.com/agda/agda/commit/c92393999d409979cc40fefbb8e45bdc35d6e55d.
I will continue to monitor the situation closely and be ready if any
problems pop up.

cheers,
Jesper

On Fri, Dec 11, 2015 at 5:53 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
wrote:

> On 11 December 2015 at 11:20, Jesper Cockx <Jesper at sikanda.be> wrote:
> > I'm writing this mail because I've come to a point where I think it makes
> > sense to integrate my work into the main Agda repository. You can find
> the
> > current status of the new unifier at
> > https://github.com/jespercockx/agda/tree/unification.
>
> > I would appreciate your feedback on my work, and I'd be glad to answer
> any
> > questions about the theory or the implementation.
>
> FYI, on your Agda master directory, you can use the following
> instructions for testing Jesper's implementation:
>
>   $ git branch -b unification
>   $ git fetch https://github.com/jespercockx/agda.git unification
>   $ git merge FETCH_HEAD
>   $ make install-bin
>
> @Jesper, I didn't find any problem testing the new unification
> algorithm on my code.
>
> Best,
>
> --
> Andrés
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20160106/6acaf3bc/attachment.html


More information about the Agda-dev mailing list