Major Section: EVENTS
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:
(progn (defun NAME FORMALS ...) (with-output :off summary (in-theory (disable NAME))) (value-triple '(:defund NAME))).Only the
:definition rule (and, for recursively defined functions,
the :induction rule) for the function are disabled. In particular,
defund does not disable either the :type-prescription or the
:executable-counterpart rule. Also, the summary for the
in-theory event is suppressed.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.)
Note that defund commands are never redundant (see redundant-events)
when the default-defun-mode is :logic, because the
in-theory event will always be executed.
See defun for documentation of defun.
