		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Stobjs-out+

Enhanced variant of stobjs-out.

Signature
(stobjs-out+ fn wrld) → result
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: result — Type (symbol-listp result).

This returns the same result as stobjs-out, but it includes a run-time check (which should always succeed) on the result that allows us to prove the return type theorem 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 depend on how it is called. This condition is part of the guard of this utility.

Definitions and Theorems

Function: stobjs-out+

(defun stobjs-out+ (fn wrld)
 (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
 (declare (xargs :guard (not (member-eq fn *stobjs-out-invalid*))))
 (let ((__function__ 'stobjs-out+))
  (declare (ignorable __function__))
  (if (not (function-symbolp fn wrld))
      (raise "The symbol ~x0 does not name a function."
             fn)
   (b* ((result (stobjs-out fn wrld)))
    (if (symbol-listp result)
        result
     (raise
      "Internal error: ~
                the STOBJS-OUT property ~x0 of ~x1 ~
                is not a true list of symbols."
      result fn))))))

Theorem: symbol-listp-of-stobjs-out+

(defthm symbol-listp-of-stobjs-out+
  (b* ((result (stobjs-out+ fn wrld)))
    (symbol-listp result))
  :rule-classes :rewrite)