Generate the named constant event.
(read-files-gen-defconst const paths preprocessor state) → (mv erp event state)
Based on the
Function:
(defun read-files-gen-defconst (const paths preprocessor state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp const) (filepath-setp paths) (or (not preprocessor) (equal :auto preprocessor) (stringp preprocessor))))) (let ((__function__ 'read-files-gen-defconst)) (declare (ignorable __function__)) (b* (((reterr) '(_) state) ((erp fileset state) (cond ((not preprocessor) (read-files-read paths state)) ((eq :auto preprocessor) (read-files-read-and-preprocess paths "cpp" state)) (t (read-files-read-and-preprocess paths preprocessor state)))) (event (cons 'defconst (cons const (cons (cons 'quote (cons fileset 'nil)) 'nil))))) (retok event state))))
Theorem:
(defthm pseudo-event-formp-of-read-files-gen-defconst.event (b* (((mv acl2::?erp acl2::?event acl2::?state) (read-files-gen-defconst const paths preprocessor state))) (pseudo-event-formp event)) :rule-classes :rewrite)