Lift defmapping-gen-appcond-thm to lists of applicability conditions.
(defmapping-gen-appcond-thms appconds appcond-thm-names thm-names$ thm-enable$ wrld) → (mv local-events exported-events)
Function:
(defun defmapping-gen-appcond-thms (appconds appcond-thm-names thm-names$ thm-enable$ wrld) (declare (xargs :guard (and (evmac-appcond-listp appconds) (symbol-symbol-alistp appcond-thm-names) (symbol-symbol-alistp thm-names$) (keyword-listp thm-enable$) (plist-worldp wrld)))) (let ((__function__ 'defmapping-gen-appcond-thms)) (declare (ignorable __function__)) (b* (((when (endp appconds)) (mv nil nil)) ((mv local-event exported-event) (defmapping-gen-appcond-thm (car appconds) appcond-thm-names thm-names$ thm-enable$ wrld)) ((mv local-events exported-events) (defmapping-gen-appcond-thms (cdr appconds) appcond-thm-names thm-names$ thm-enable$ wrld))) (mv (cons local-event local-events) (cons exported-event exported-events)))))