		Search-engine friendly clone of the ACL2 documentation.

Defequal-implementation

Defequal-fn

Check redundancy, process the inputs, generated the events.

Signature
(defequal-fn 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 call ctx state) → (mv erp event state)
Arguments: left-present — Guard (booleanp left-present).; right-present — Guard (booleanp right-present).; call — Guard (pseudo-event-formp call).
Returns: event — A pseudo-event-formp.

Definitions and Theorems

Function: defequal-fn

(defun defequal-fn (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 call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (booleanp left-present)
                              (booleanp right-present)
                              (pseudo-event-formp call))))
  (let ((__function__ 'defequal-fn))
    (declare (ignorable __function__))
    (b* ((expansion? (defequal-redundant? call (w state)))
         ((when expansion?)
          (b* (((run-when show-only)
                (cw "~x0~|" expansion?)))
            (cw "~%The call ~x0 is redundant.~%" call)
            (value '(value-triple :invisible))))
         ((er (list x1...xn left-to-right right-to-left))
          (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))
         (event (defequal-gen-everything
                     name
                     left right x1...xn enable verify-guards
                     left-to-right left-to-right-enable
                     right-to-left right-to-left-enable
                     print show-only call)))
      (value event))))