Check if a named function has no input or output stobjs.
The function must not be in
See no-stobjs-p+ for an enhanced variant of this utility.
(defun no-stobjs-p (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (declare (xargs :guard (not (member-eq fn *stobjs-out-invalid*)))) (let ((__function__ 'no-stobjs-p)) (declare (ignorable __function__)) (and (all-nils (stobjs-in fn wrld)) (all-nils (stobjs-out fn wrld)))))
(defthm booleanp-of-no-stobjs-p (b* ((yes/no (no-stobjs-p fn wrld))) (booleanp yes/no)) :rule-classes :rewrite)