		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-newp-of-new-name

Process the :newp-of-new-name input.

Signature
(expdata-process-newp-of-new-name newp-of-new-name new$ names-to-avoid ctx state) → (mv erp result state)
Arguments: new$ — Guard (symbolp new$).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — A list (newp-of-new$ updated-new-names-to-avoid) satisfying (typed-tuplep symbolp symbol-listp result).

Definitions and Theorems

Function: expdata-process-newp-of-new-name

(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))))))