		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-appcond-thms

Lift defmapping-gen-appcond-thm to lists of applicability conditions.

Signature
(defmapping-gen-appcond-thms appconds appcond-thm-names thm-names$ thm-enable$ wrld) → (mv local-events exported-events)
Arguments: appconds — Guard (evmac-appcond-listp appconds).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; thm-names$ — Guard (symbol-symbol-alistp thm-names$).; thm-enable$ — Guard (keyword-listp thm-enable$).; wrld — Guard (plist-worldp wrld).
Returns: local-events — A pseudo-event-form-listp.; exported-events — A pseudo-event-form-listp.

Definitions and Theorems

Function: defmapping-gen-appcond-thms

(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)))))