Process the
(defequal-process-left-to-right-name left-to-right-name name left right names-to-avoid ctx state) → (mv erp result state)
Function:
(defun defequal-process-left-to-right-name (left-to-right-name name left right names-to-avoid ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp name) (symbolp left) (symbolp right) (symbol-listp names-to-avoid)))) (let ((__function__ 'defequal-process-left-to-right-name)) (declare (ignorable __function__)) (b* (((er &) (ensure-value-is-symbol$ left-to-right-name "The :LEFT-TO-RIGHT input" t nil)) (left-to-right (if (eq left-to-right-name :auto) (packn-pos (list left '-to- right) name) left-to-right-name)) ((er names-to-avoid) (ensure-symbol-is-fresh-event-name$ left-to-right (msg "The name ~x0 specified by :LEFT-TO-RIGHT-NAME" left-to-right) 'function names-to-avoid t nil))) (value (list left-to-right names-to-avoid)))))