Process the inputs and generate the constant event.
(print-files-process-inputs-and-gen-defconst args wrld) → (mv erp event)
Function:
(defun print-files-process-inputs-and-gen-defconst (args wrld) (declare (xargs :guard (and (true-listp args) (plist-worldp wrld)))) (let ((__function__ 'print-files-process-inputs-and-gen-defconst)) (declare (ignorable __function__)) (b* (((reterr) '(_)) ((erp const-fileset value-transunits) (print-files-process-inputs args wrld)) (event (print-files-gen-defconst const-fileset value-transunits))) (retok event))))
Theorem:
(defthm pseudo-event-formp-of-print-files-process-inputs-and-gen-defconst.event (b* (((mv acl2::?erp acl2::?event) (print-files-process-inputs-and-gen-defconst args wrld))) (pseudo-event-formp event)) :rule-classes :rewrite)