		Search-engine friendly clone of the ACL2 documentation.

Parteval-input-processing

Parteval-process-thm-name

Process the :thm-name input.

Signature
(parteval-process-thm-name thm-name old$ new-name$ ctx state) → (mv erp thm-name$ state)
Arguments: old$ — Guard (symbolp old$).; new-name$ — Guard (symbolp new-name$).
Returns: thm-name$ — A symbolp to use for the theorem that relates the old and new functions.

Definitions and Theorems

Function: parteval-process-thm-name

(defun parteval-process-thm-name (thm-name old$ new-name$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (symbolp new-name$))))
 (let ((__function__ 'parteval-process-thm-name))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-value-is-symbol$ thm-name "The :THM-NAME input" t nil))
    (name (if (eq thm-name :auto)
              (make-paired-name old$ new-name$ 2 (w state))
            thm-name))
    (description
     (msg
      "The name ~x0 of the theorem ~
                          that relates the target function ~x1 ~
                          to the new function ~x2, ~
                          ~@3,"
      name old$ new-name$
      (if
       (eq thm-name :auto)
       "automatically generated ~
                              since the :THM-NAME input ~
                              is (perhaps by default) :AUTO"
       "supplied as the :THM-NAME input")))
    ((er &)
     (ensure-symbol-new-event-name$ name description t nil))
    ((er &)
     (ensure-symbol-different$
      name new-name$
      (msg
       "the name ~x0 of the new function ~
                      (determined by the :NEW-NAME input)."
       new-name$)
      description t nil)))
   (value name))))