[Agda-dev] A new unifier for case splitting

[Andrés Sicard-Ramírez]

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