		Search-engine friendly clone of the ACL2 documentation.

Split-fn-when-event-generation

Split-fn-when-process-inputs-and-gen-everything

Process the inputs and generate the events.

Signature
(split-fn-when-process-inputs-and-gen-everything const-old const-new triggers 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: split-fn-when-process-inputs-and-gen-everything

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

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

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

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

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