Project the execution correctness theorems out of a function information alist, for the functions among a given list.
(atc-symbol-fninfo-alist-to-correct-thms prec-fns among) → thms
This is similar to atc-symbol-fninfo-alist-to-result-thms. See that function's documentation for more details.
Function:
(defun atc-symbol-fninfo-alist-to-correct-thms (prec-fns among) (declare (xargs :guard (and (atc-symbol-fninfo-alistp prec-fns) (symbol-listp among)))) (let ((__function__ 'atc-symbol-fninfo-alist-to-correct-thms)) (declare (ignorable __function__)) (cond ((endp prec-fns) nil) ((member-eq (caar prec-fns) among) (cons (atc-fn-info->correct-thm (cdr (car prec-fns))) (atc-symbol-fninfo-alist-to-correct-thms (cdr prec-fns) among))) (t (atc-symbol-fninfo-alist-to-correct-thms (cdr prec-fns) among)))))
Theorem:
(defthm symbol-listp-of-atc-symbol-fninfo-alist-to-correct-thms (b* ((thms (atc-symbol-fninfo-alist-to-correct-thms prec-fns among))) (symbol-listp thms)) :rule-classes :rewrite)