[Agda] Agda implementation of McBride's unification paper?
asai at is.ocha.ac.jp
Mon Nov 18 00:26:52 CET 2013
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!
More information about the Agda