		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Number-of-results+

Enhanced variant of number-of-results.

Signature
(number-of-results+ fn wrld) → n
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: n — Type (posp n).

This returns the same result as number-of-results, but it includes a run-time check (which should always succeed) on the result that allows us to prove a tighter return type theorem than number-of-results without strengthening the guard on wrld. Furthermore, this utility causes an error if called on a symbol that does not name a function.

The function must not be in *stobjs-out-invalid*, because in that case its output stobjs, and therefore the number of its results, depend on how it is called. This condition is part of the guard 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__))
  (cond
   ((not (function-symbolp fn wrld))
    (prog2$ (raise "The symbol ~x0 does not name a function."
                   fn)
            1))
   (t
    (b* ((result (number-of-results fn wrld)))
     (if (posp result)
         result
      (prog2$
       (raise
        "Internal error: ~
                               the STOBJS-OUT property of ~x0 is empty."
        fn)
       1)))))))

Theorem: posp-of-number-of-results+

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