Process the inputs and generate the constant event.
(read-files-process-inputs-and-gen-defconst args state) → (mv erp event state)
Function:
(defun read-files-process-inputs-and-gen-defconst (args state) (declare (xargs :stobjs (state))) (declare (xargs :guard (true-listp args))) (let ((__function__ 'read-files-process-inputs-and-gen-defconst)) (declare (ignorable __function__)) (b* (((reterr) '(_) state) ((erp const paths preprocessor) (read-files-process-inputs args)) ((erp event state) (read-files-gen-defconst const paths preprocessor state))) (retok event state))))
Theorem:
(defthm pseudo-event-formp-of-read-files-process-inputs-and-gen-defconst.event (b* (((mv acl2::?erp acl2::?event acl2::?state) (read-files-process-inputs-and-gen-defconst args state))) (pseudo-event-formp event)) :rule-classes :rewrite)