(look-up-return-vals fn world) returns the
Function:
(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:
(defthm symbol-listp-of-look-up-return-vals (symbol-listp (look-up-return-vals fn world)))