Number of values returned by a named function.
(number-of-results fn wrld) → n
This is 1, unless the function uses mv (directly, or indirectly by calling another function that does) to return multiple values.
The number of results of the function is the length of its stobjs-out list.
The function must not be in
See number-of-results+ for an enhanced variant of this utility.
Function:
(defun number-of-results (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (declare (xargs :guard (not (member-eq fn *stobjs-out-invalid*)))) (let ((__function__ 'number-of-results)) (declare (ignorable __function__)) (len (stobjs-out fn wrld))))
Theorem:
(defthm natp-of-number-of-results (b* ((n (number-of-results fn wrld))) (natp n)) :rule-classes :rewrite)