Major Section: EVENTS
Defpun is a macro developed by Pete Manolios and J Moore that allows
tail-recursive definitions. It is defined in community book
books/misc/defpun.lisp, so to use it, execute the following event.
(include-book "misc/defpun" :dir :system)Details of defpun are provided by Manolios and Moore in the ``Partial Functions in ACL2'' published with the ACL2 2000 workshop; see http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/. Also see http://www.cs.utexas.edu/users/moore/publications/defpun/index.html.
A variant, defp, has been developed by Matt Kaufmann to allow more
general forms of tail recursion. If defpun doesn't work for you, try
defp by first executing the following event.
(include-book "misc/defp" :dir :system)
Sandip Ray has contributed a variant of defpun, defpun-exec, that
supports executability. See community book
books/defexec/defpun-exec/defpun-exec.lisp:
(include-book "defexec/defpun-exec/defpun-exec" :dir :system)He has also contributed community book
books/misc/misc2/defpun-exec-domain-example.lisp, for functions that are
uniquely defined in a particular domain.
