<div dir="ltr">Hey Kenichi,<div><br></div><div>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:</div>
<div><br></div><div><a href="https://github.com/pepijnkokke/first-order-unification-in-agda" target="_blank">https://github.com/pepijnkokke/first-order-unification-in-agda</a><br></div><div><br></div><div>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.</div>
<div><br></div><div>Pepijn</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On 18 November 2013 00:26, Kenichi Asai <span dir="ltr"><<a href="mailto:asai@is.ocha.ac.jp" target="_blank">asai@is.ocha.ac.jp</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear all,<br>
<br>
I wonder if there is an agda implementation of Conor McBride's paper<br>
"First-order unification by structural recursion". Any information is<br>
welcome.<br>
<br>
The Data.List.Countdown module in the standard library appears to be<br>
related to the paper. If there is any document on how to use it,<br>
please let me know. (I am rather new to agda, and it is a bit<br>
difficult for me to read through the module, although I am trying.)<br>
<br>
Thank you in advance!<br>
<br>
Sincerely,<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Kenichi Asai<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>