Enhanced variant of classes.
(classes+ thm wrld) → classes
This returns the same result as classes,
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 classes+ (thm wrld) (declare (xargs :guard (and (symbolp thm) (plist-worldp wrld)))) (let ((__function__ 'classes+)) (declare (ignorable __function__)) (if (not (theorem-symbolp thm wrld)) (raise "The symbol ~x0 does not name a theorem." thm) (b* ((result (classes thm wrld))) (if (keyword-to-keyword-value-list-alistp result) result (raise "Internal error: ~ the rule classes ~x0 of ~x1 are not an alist from keywords to keyword-value lists." result thm))))))
(defthm keyword-to-keyword-value-list-alistp-of-classes+ (b* ((classes (classes+ thm wrld))) (keyword-to-keyword-value-list-alistp classes)) :rule-classes :rewrite)