If the check fails,
As explained here, we consult the pe-table.
If the defun-sk is generated by some other macros
that also extends the table,
the defun-sk form is not the only one
This utility causes an error if called on a symbol that is not a function symbol.
(defun defun-sk-p (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'defun-sk-p)) (declare (ignorable __function__)) (b* (((unless (function-symbolp fn wrld)) (raise "The symbol ~x0 does not name a function." fn)) (table (table-alist 'pe-table wrld)) (entry (cdr (assoc-eq fn table))) (last-number+form (car (last entry))) (last-form (cdr last-number+form))) (if (eq (car last-form) 'defun-sk) last-form nil))))