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

[Pepijn Kokke]

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
look:

https://github.com/pepijnkokke/first-order-unification-in-agda

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
complete.

Pepijn


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