		Search-engine friendly clone of the ACL2 documentation.

Defequal-input-processing

Defequal-process-name

Process the name input.

Signature
(defequal-process-name name names-to-avoid ctx state) → (mv erp updated-names-to-avoid state)
Arguments: names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: updated-names-to-avoid — Always symbol-listp.

Definitions and Theorems

Function: defequal-process-name

(defun defequal-process-name (name names-to-avoid ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (symbol-listp names-to-avoid)))
  (let ((__function__ 'defequal-process-name))
    (declare (ignorable __function__))
    (b* (((er &)
          (ensure-value-is-symbol$ name "The NAME input" t nil))
         ((er names-to-avoid)
          (ensure-symbol-is-fresh-event-name$
               name (msg "The NAME input ~x0" name)
               'function
               names-to-avoid t nil)))
      (value names-to-avoid))))