Major Section: EVENTS
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
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
definitionrule (and, for recursively defined functions, the
inductionrule) for the function are disabled, and the summary for the
in-theoryevent is suppressed.
defund commands are never redundant (see redundant-events).
If the function has already been defined, then the
will still be executed.
See defun for documentation of