Process the
(expdata-process-newp-of-new-name newp-of-new-name new$ names-to-avoid ctx state) → (mv erp result state)
Function:
(defun expdata-process-newp-of-new-name (newp-of-new-name new$ names-to-avoid ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp new$) (symbol-listp names-to-avoid)))) (let ((__function__ 'expdata-process-newp-of-new-name)) (declare (ignorable __function__)) (b* (((er &) (ensure-value-is-symbol$ newp-of-new-name "The :NEWP-OF-NEW-NAME input" t nil)) (newp-of-new$ (case newp-of-new-name (:auto (add-suffix new$ "-NEW-REPRESENTATION")) (t newp-of-new-name))) (description (msg "The name ~x0 of the theorem asserting that ~ the new function ~x1 maps ~ arguments in the new representation ~ to results in the new representation, ~@2," newp-of-new$ new$ (if (eq newp-of-new-name :auto) "automatically generated ~ since the :NEWP-OF-NEW-NAME input ~ is (perhaps by default) :AUTO" "supplied as the :NEWP-OF-NEW-NAME input"))) (error-msg? (fresh-namep-msg-weak newp-of-new$ nil (w state))) ((when error-msg?) (er-soft+ ctx t nil "~@0 must be a valid fresh theorem name. ~@1" description error-msg?)) ((er &) (ensure-value-is-not-in-list$ newp-of-new$ names-to-avoid (msg "among the names ~x0 of other events ~ generated by this transformation" names-to-avoid) description t nil))) (value (list newp-of-new$ (cons newp-of-new$ names-to-avoid))))))