DEFUND

define a function symbol and then disable it
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-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.

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.