Generate the named constant event.
(print-files-gen-defconst const-fileset value-transunits) → event
Function:
(defun print-files-gen-defconst (const-fileset value-transunits) (declare (xargs :guard (and (symbolp const-fileset) (transunit-ensemblep value-transunits)))) (let ((__function__ 'print-files-gen-defconst)) (declare (ignorable __function__)) (b* ((fileset (print-fileset value-transunits)) (event (cons 'defconst (cons const-fileset (cons (cons 'quote (cons fileset 'nil)) 'nil))))) event)))
Theorem:
(defthm pseudo-event-formp-of-print-files-gen-defconst (b* ((event (print-files-gen-defconst const-fileset value-transunits))) (pseudo-event-formp event)) :rule-classes :rewrite)