Defund-nx
Define a disabled non-executable function symbol
Use defund-nx instead of defun-nx when you want to
disable the definition of a function symbol immediately after defining
it in :logic mode. In all other respects, defund-nx has the
same behavior as defun-nx; See defun-nx for details. Also see
defund.