Process the
(process-input-new-to-old-name new-to-old-name new-to-old-name-present old new names-to-avoid ctx state) → (mv erp result state)
This is quite analogous to process-input-old-to-new-name,
but for the
Function:
(defun process-input-new-to-old-name (new-to-old-name new-to-old-name-present old new names-to-avoid ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (booleanp new-to-old-name-present) (symbolp old) (symbolp new) (symbol-listp names-to-avoid)))) (let ((__function__ 'process-input-new-to-old-name)) (declare (ignorable __function__)) (b* ((wrld (w state)) ((er &) (if new-to-old-name-present (ensure-value-is-symbol$ new-to-old-name "The :NEW-TO-OLD-NAME input" t nil) (value nil))) (name (if (or (not new-to-old-name-present) (keywordp new-to-old-name)) (b* ((kwd (if new-to-old-name-present new-to-old-name (get-default-input-new-to-old-name wrld)))) (intern-in-package-of-symbol (concatenate 'string (symbol-name new) (symbol-name kwd) (symbol-name old)) new)) new-to-old-name)) (description (msg "The name ~x0 of the theorem ~ that rewrites the new function ~x1 ~ in terms of the old function ~x2, ~ specified (perhaps by default) ~ by the :NEW-TO-OLD-NAME input ~x3," name new old new-to-old-name)) (error-msg? (fresh-namep-msg-weak name nil wrld)) ((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$ name names-to-avoid (msg "among the names ~x0 of other events ~ generated by this transformation" names-to-avoid) description t nil))) (value (list name (cons name names-to-avoid))))))