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

[Dr. ERDI Gergo]

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.

Hi,

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

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

Bye,
 	Gergo

-- 

   .--= 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?