		Search-engine friendly clone of the ACL2 documentation.

Defequal-table

Defequal-redundant?

Check if a call of defequal is redundant, returning the associated expansion if it is.

Signature
(defequal-redundant? call wrld) → event?
Arguments: call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: event? — Type (maybe-pseudo-event-formp event?).

Definitions and Theorems

Function: defequal-redundant?

(defun defequal-redundant? (call wrld)
 (declare (xargs :guard (and (pseudo-event-formp call)
                             (plist-worldp wrld))))
 (let ((__function__ 'defequal-redundant?))
  (declare (ignorable __function__))
  (b* ((table (table-alist+ 'defequal-table wrld)
)
       (call (defequal-trim-call call))
       (pair? (assoc-equal call table)))
   (if pair?
    (b* ((expansion (cdr pair?)))
     (if (pseudo-event-formp expansion)
         expansion
      (raise
       "Internal error: ~
                    the DEFEQUAL table associates the call ~x0 ~
                    with a value ~x1 that is not a pseudo event form."
       call expansion)))
    nil))))

Theorem: maybe-pseudo-event-formp-of-defequal-redundant?

(defthm maybe-pseudo-event-formp-of-defequal-redundant?
  (b* ((event? (defequal-redundant? call wrld)))
    (maybe-pseudo-event-formp event?))
  :rule-classes :rewrite)