		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-implementation

Deffoldred-process-inputs-and-gen-everything

Process the inputs and generate the events.

Signature
(deffoldred-process-inputs-and-gen-everything args wrld) → (mv erp event)
Arguments: args — Guard (true-listp args).; wrld — Guard (plist-worldp wrld).
Returns: event — Type (acl2::pseudo-event-formp event).

Definitions and Theorems

Function: deffoldred-process-inputs-and-gen-everything

(defun deffoldred-process-inputs-and-gen-everything (args wrld)
 (declare (xargs :guard (and (true-listp args)
                             (plist-worldp wrld))))
 (let ((__function__ 'deffoldred-process-inputs-and-gen-everything))
   (declare (ignorable __function__))
   (b* (((reterr) '(_))
        (fty-table (acl2::table-alist+ 'flextypes-table
                                       wrld))
        ((erp suffix types targets extra-args
              result default combine overrides
              parents-presentp parents short-presentp
              short long-presentp long print)
         (deffoldred-process-inputs args fty-table)))
     (retok (deffoldred-gen-everything
                 suffix
                 types targets extra-args result default
                 combine overrides parents-presentp
                 parents short-presentp short
                 long-presentp long fty-table print)))))

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

(defthm
 pseudo-event-formp-of-deffoldred-process-inputs-and-gen-everything.event
 (b* (((mv ?erp acl2::?event)
       (deffoldred-process-inputs-and-gen-everything args wrld)))
   (acl2::pseudo-event-formp event))
 :rule-classes :rewrite)