[Agda] Agda implementation of McBride's unification paper?

Pepijn Kokke pepijn.kokke at gmail.com
Mon Nov 18 18:11:27 CET 2013

Hey Kenichi,

I have a working implementation of McBride's unification algorithm that I'm
using it myself to implement proof search in Agda. I've taken the
unification part out and put it on GitHub, in case you would like to have a


So far I've made some progress towards proving it's correctness (to be
found in Unification/Correctness) but these proofs are still far from


On 18 November 2013 00:26, Kenichi Asai <asai at is.ocha.ac.jp> wrote:

> Dear all,
> I wonder if there is an agda implementation of Conor McBride's paper
> "First-order unification by structural recursion".  Any information is
> welcome.
> The Data.List.Countdown module in the standard library appears to be
> related to the paper.  If there is any document on how to use it,
> please let me know.  (I am rather new to agda, and it is a bit
> difficult for me to read through the module, although I am trying.)
> Thank you in advance!
> Sincerely,
> --
> Kenichi Asai
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131118/8c5abb42/attachment.html

More information about the Agda mailing list