Major Section: EVENTS
Defpun is a macro developed by Pete Manolios and J Moore that allows
tail-recursive definitions. It is defined in distributed 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
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
supports executability. See distributed book
(include-book "defexec/defpun-exec/defpun-exec" :dir :system)He has also contributed book
books/misc/misc2/defpun-exec-domain-example.lisp, for functions that are uniquely defined in a particular domain.