Generate the named constant event.
(parse-files-gen-defconst const-transunits value-fileset gcc) → (mv erp event)
Function:
(defun parse-files-gen-defconst (const-transunits value-fileset gcc) (declare (xargs :guard (and (symbolp const-transunits) (filesetp value-fileset) (booleanp gcc)))) (let ((__function__ 'parse-files-gen-defconst)) (declare (ignorable __function__)) (b* (((reterr) '(_)) ((erp tunits) (parse-fileset value-fileset gcc)) (event (cons 'defconst (cons const-transunits (cons (cons 'quote (cons tunits 'nil)) 'nil))))) (retok event))))
Theorem:
(defthm pseudo-event-formp-of-parse-files-gen-defconst.event (b* (((mv acl2::?erp acl2::?event) (parse-files-gen-defconst const-transunits value-fileset gcc))) (pseudo-event-formp event)) :rule-classes :rewrite)