Combine evmac-appcond-theorem-list and evmac-ensure-no-extra-hints.
(evmac-appcond-theorems-no-extra-hints appconds hints names-to-avoid print ctx state) → (mv erp val state)
This function automates the coding pattern in which first one calls evmac-appcond-theorem-list and then evmac-ensure-no-extra-hints on the remaining hints. This combining function returns no hints result.
Function:
(defun evmac-appcond-theorems-no-extra-hints (appconds hints names-to-avoid print ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (evmac-appcond-listp appconds) (evmac-input-hints-p hints) (symbol-listp names-to-avoid) (evmac-input-print-p print)))) (let ((__function__ 'evmac-appcond-theorems-no-extra-hints)) (declare (ignorable __function__)) (b* (((mv events thm-names remaining-hints updated-names-to-avoid) (evmac-appcond-theorem-list appconds hints names-to-avoid print ctx state)) ((er & :iferr (list nil nil nil)) (evmac-ensure-no-extra-hints remaining-hints ctx state))) (value (list events thm-names updated-names-to-avoid)))))
Theorem:
(defthm return-type-of-evmac-appcond-theorems-no-extra-hints.val (implies (and (evmac-appcond-listp appconds) (symbol-listp names-to-avoid)) (b* (((mv ?erp ?val ?state) (evmac-appcond-theorems-no-extra-hints appconds hints names-to-avoid print ctx state))) (std::tuple (events pseudo-event-form-listp) (thm-names keyword-symbol-alistp) (updated-names-to-avoid symbol-listp) val))) :rule-classes :rewrite)