		Search-engine friendly clone of the ACL2 documentation.

Split-fn-event-generation

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

Process the inputs and generate the events.

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

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

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

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

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

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