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

Kenichi Asai asai at is.ocha.ac.jp
Mon Nov 18 00:26:52 CET 2013

Dear all,

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

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!


Kenichi Asai

More information about the Agda mailing list