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