		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-implementation

Deffold-map-process-inputs-and-gen-everything

Process the inputs and generate the events.

Signature
(deffold-map-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: deffold-map-process-inputs-and-gen-everything

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

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

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