		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Number-of-results

Number of values returned by a named function.

Signature
(number-of-results fn wrld) → n
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: n — Actually always a posp.
Type (natp 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 *stobjs-out-invalid*, because in that case the number of its results depends on how it is called.

See number-of-results+ for an enhanced variant of this utility.

Definitions and Theorems

Function: number-of-results

(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: natp-of-number-of-results

(defthm natp-of-number-of-results
        (b* ((n (number-of-results fn wrld)))
            (natp n))
        :rule-classes :rewrite)