		Search-engine friendly clone of the ACL2 documentation.

Wrap-fn-event-generation

Wrap-fn-process-inputs-and-gen-everything

Process the inputs and generate the events.

Signature
(wrap-fn-process-inputs-and-gen-everything const-old const-new targets wrld) → (mv er? event)
Arguments: wrld — Guard (plist-worldp wrld).
Returns: er? — Type (maybe-msgp er?).; event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: wrap-fn-process-inputs-and-gen-everything

(defun wrap-fn-process-inputs-and-gen-everything
       (const-old const-new targets wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (b* (((reterr) '(_))
       ((erp code const-new targets)
        (wrap-fn-process-inputs const-old const-new targets wrld))
       ((erp event)
        (wrap-fn-gen-everything code const-new targets)))
    (retok event)))

Theorem: maybe-msgp-of-wrap-fn-process-inputs-and-gen-everything.er?

(defthm maybe-msgp-of-wrap-fn-process-inputs-and-gen-everything.er?
  (b* (((mv ?er? acl2::?event)
        (wrap-fn-process-inputs-and-gen-everything
             const-old const-new targets wrld)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-wrap-fn-process-inputs-and-gen-everything.event

(defthm
 pseudo-event-formp-of-wrap-fn-process-inputs-and-gen-everything.event
 (b* (((mv ?er? acl2::?event)
       (wrap-fn-process-inputs-and-gen-everything
            const-old const-new targets wrld)))
   (pseudo-event-formp event))
 :rule-classes :rewrite)