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

Dr. ERDI Gergo gergo at erdi.hu
Mon Nov 18 02:15:11 CET 2013

On Mon, 18 Nov 2013, Kenichi Asai wrote:

> I wonder if there is an agda implementation of Conor McBride's paper
> "First-order unification by structural recursion".  Any information is
> welcome.


I've started doing that a while ago, but only got far enough to define 
'mgu' and prove the properties of thin vs. thick and substitution. I've 
lost interest before proving the main theorem of 'mgu' returning an actual 

I've uploaded now my code to https://github.com/gergoerdi/mgu-agda so 
check it out if you're interested.



   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
Did you ever wonder if your mom just gave dad a blowjob right before she kissed you good night?

More information about the Agda mailing list