		Search-engine friendly clone of the ACL2 documentation.

Support

Look-up-return-vals

(look-up-return-vals fn world) returns the stobjs-out property for fn. This is a list that may contain nils and ACL2::stobj names, with the same length as the number of return vals for fn.

Definitions and Theorems

Function: look-up-return-vals

(defun look-up-return-vals (fn world)
 (declare (xargs :guard (and (symbolp fn)
                             (plist-worldp world))))
 (b*
  ((__function__ 'look-up-return-vals)
   (stobjs-out (getprop fn 'acl2::stobjs-out
                        :bad 'acl2::current-acl2-world
                        world))
   ((when (eq stobjs-out :bad))
    (raise "Can't look up stobjs-out for ~x0!" fn)
    '(nil))
   ((unless (and (consp stobjs-out)
                 (symbol-listp stobjs-out)))
    (raise
     "Expected stobjs-out to be a non-empty symbol-list, but ~
                  found ~x0."
     stobjs-out)
    '(nil)))
  stobjs-out))

Theorem: symbol-listp-of-look-up-return-vals

(defthm symbol-listp-of-look-up-return-vals
  (symbol-listp (look-up-return-vals fn world)))