Number of results returned by a function.
(atj-number-of-results fn wrld) → numres
This is similar to number-of-results+,
but that function has a guard disallowing the function symbol
to be a member of the built-in constant
Function:
(defun atj-number-of-results (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'atj-number-of-results)) (declare (ignorable __function__)) (cond ((member-eq fn *stobjs-out-invalid*) 1) (t (number-of-results+ fn wrld)))))
Theorem:
(defthm posp-of-atj-number-of-results (b* ((numres (atj-number-of-results fn wrld))) (posp numres)) :rule-classes :rewrite)