DEFPUN

define a tail-recursive function symbol
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.