		Search-engine friendly clone of the ACL2 documentation.

Specialize-event-generation

Specialize-process-inputs-and-gen-everything

Process the inputs and generate the events.

Signature
(specialize-process-inputs-and-gen-everything const-old const-new target param const 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: specialize-process-inputs-and-gen-everything

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

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

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

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

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