Defund
Define a function symbol and then disable it
Use defund instead of defun when you want to disable a function immediately after its definition in :logic
mode. This macro has been provided for users who prefer working in a mode
where functions are only enabled when explicitly directed by :in-theory. Specifically, the form
(defund NAME FORMALS ...)
expands to the following, except that some output is inhibited for the
in-theory event:
(progn
(defun NAME FORMALS ...)
(in-theory (disable NAME))
(value-triple '(:defund NAME))).
Only the :definition rule and, for recursively defined
functions, the :induction rule are disabled for the function.
In particular, defund does not disable either the :type-prescription or the :executable-counterpart rule.
If the function is defined in :program mode, either because
the default-defun-mode is :program or because :mode
:program has been specified in an xargs form of a declare
form, then no in-theory event is executed. (More precisely, in-theory events are ignored when the default-defun-mode is
:program, and if :mode :program is specified then
defund does not generate an in-theory event.)
Defund events are generally not redundant, because the generated
in-theory event is not redundant. This default can be changed; see
set-in-theory-redundant-okp.
See defun for documentation of defun.
