Major Section: EVENTS
Use defund instead of defun when you want to disable a function
immediately after its definition. 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 NAME)).Only the
:definition rule (and, for recursively defined functions,
the :induction rule) for the function are disabled, and the summary
for the in-theory event is suppressed.
Note that defund commands are never redundant (see redundant-events).
If the function has already been defined, then the in-theory event
will still be executed.
See defun for documentation of defun.