		Search-engine friendly clone of the ACL2 documentation.

Defequal-input-processing

Defequal-process-inputs

Process all the inputs.

Signature
(defequal-process-inputs name left left-present right right-present vars enable verify-guards left-to-right-name left-to-right-enable right-to-left-name right-to-left-enable print show-only ctx state) → (mv erp result state)
Arguments: left-present — Guard (booleanp left-present).; right-present — Guard (booleanp right-present).
Returns: result — A tuple (x1...xn left-to-right right-to-left updated-names-to-avoid) satisfying (typed-tuplep symbol-listp symbol-listp symbolp symbolp symbol-listp result).

Definitions and Theorems

Function: defequal-process-inputs

(defun defequal-process-inputs
       (name left left-present right
             right-present vars enable verify-guards
             left-to-right-name left-to-right-enable
             right-to-left-name right-to-left-enable
             print show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp left-present)
                             (booleanp right-present))))
 (let ((__function__ 'defequal-process-inputs))
  (declare (ignorable __function__))
  (b*
   ((names-to-avoid nil)
    ((er names-to-avoid)
     (defequal-process-name name names-to-avoid ctx state))
    ((er n)
     (defequal-process-left-and-right
          left left-present right
          right-present verify-guards ctx state))
    ((er x1...xn)
     (defequal-process-vars vars name left right n ctx state))
    ((er &)
     (ensure-value-is-boolean$ enable "The :ENABLE input" t nil))
    ((er &)
     (ensure-value-is-boolean$ verify-guards
                               "The :VERIFY-GUARDS input" t nil))
    ((er (list left-to-right names-to-avoid))
     (defequal-process-left-to-right-name
          left-to-right-name name
          left right names-to-avoid ctx state))
    ((er &)
     (ensure-value-is-boolean$ left-to-right-enable
                               "The :LEFT-TO-RIGHT-ENABLE input"
                               t nil))
    ((er (list right-to-left names-to-avoid))
     (defequal-process-right-to-left-name
          right-to-left-name name
          left right names-to-avoid ctx state))
    ((er &)
     (ensure-value-is-boolean$ right-to-left-enable
                               "The :RIGHT-TO-LEFT-ENABLE input"
                               t nil))
    ((when (and left-to-right-enable
                right-to-left-enable))
     (er-soft+
      ctx t nil
      "The :LEFT-TO-RIGHT-ENABLE and :RIGHT-TO-LEFT-ENABLE inputs ~
                   are both T; this is disallowed."))
    ((er &)
     (evmac-process-input-print print ctx state))
    ((er &)
     (evmac-process-input-show-only show-only ctx state)))
   (value (list x1...xn left-to-right
                right-to-left names-to-avoid)))))