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 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.