Several Coq libraries and extensions support the definition of non-structural recursive functions using well-founded orderings for termination. After pointing out some drawbacks of these existing approaches, we advocate going back to the basics and defining recursive functions by explicit structural induction on a proof of accessibility of the principal recursive argument.
[ bib | At HAL | Local copy ] Back
This file was generated by bibtex2html 1.99.