Enhanced variant of no-stobjs-p.
(no-stobjs-p+ fn wrld) → yes/no
This returns the same result as no-stobjs-p, but it is guard-verified and it causes an error (via stobjs-in+ if called on a symbol that does not name a function.
The function must not be in
(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)