Enhanced variant of thm-formula.
(thm-formula+ thm wrld) → formula
This returns the same result as thm-formula,
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
(defun thm-formula+ (thm wrld) (declare (xargs :guard (and (symbolp thm) (plist-worldp wrld)))) (let ((__function__ 'thm-formula+)) (declare (ignorable __function__)) (if (not (theorem-symbolp thm wrld)) (raise "The symbol ~x0 does not name a theorem." thm) (b* ((result (thm-formula thm wrld))) (if (pseudo-termp result) result (raise "Internal error: ~ the FORMULA property ~x0 of ~x1 is not a pseudo-term." result thm))))))
(defthm pseudo-termp-of-thm-formula+ (b* ((formula (thm-formula+ thm wrld))) (pseudo-termp formula)) :rule-classes :rewrite)