		Search-engine friendly clone of the ACL2 documentation.

Defmapping-implementation

Defmapping-fn

Check redundancy, process the inputs, and generate the event to submit.

Signature
(defmapping-fn name doma domb alpha beta beta-of-alpha-thm alpha-of-beta-thm guard-thms unconditional thm-names thm-enable hints print show-only call ctx state) → (mv erp event state)
Arguments: call — Guard (pseudo-event-formp call).
Returns: event — A pseudo-event-formp.

Definitions and Theorems

Function: defmapping-fn

(defun defmapping-fn (name doma domb alpha beta beta-of-alpha-thm
                           alpha-of-beta-thm guard-thms
                           unconditional thm-names thm-enable
                           hints print show-only call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (pseudo-event-formp call)))
  (let ((__function__ 'defmapping-fn))
    (declare (ignorable __function__))
    (b* (((er redundant?)
          (defmapping-check-redundancy
               name print show-only call ctx state))
         ((when redundant?)
          (value '(value-triple :invisible)))
         ((er (list doma$ domb$ alpha$
                    beta$ thm-names$ thm-enable$ hints$))
          (defmapping-process-inputs
               name
               doma domb alpha beta beta-of-alpha-thm
               alpha-of-beta-thm guard-thms
               unconditional thm-names thm-enable
               hints print show-only ctx state)))
      (defmapping-gen-everything name doma$ domb$ alpha$ beta$
                                 beta-of-alpha-thm alpha-of-beta-thm
                                 guard-thms unconditional
                                 thm-names$ thm-enable$ hints$
                                 print show-only call ctx state))))