		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Stobjs-in+

Enhanced variant of stobjs-in.

Signature
(stobjs-in+ 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-in, 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.

Definitions and Theorems

Function: stobjs-in+

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

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

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