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