		Search-engine friendly clone of the ACL2 documentation.

Defequal-table

Defequal-record-call

Table event to record a call of defequal.

Signature
(defequal-record-call call expansion) → table-event
Arguments: call — Guard (pseudo-event-formp call).; expansion — Guard (pseudo-event-formp expansion).
Returns: table-event — Type (pseudo-event-formp table-event).

Definitions and Theorems

Function: defequal-record-call

(defun defequal-record-call (call expansion)
  (declare (xargs :guard (and (pseudo-event-formp call)
                              (pseudo-event-formp expansion))))
  (let ((__function__ 'defequal-record-call))
    (declare (ignorable __function__))
    (b* ((call (defequal-trim-call call)))
      (cons 'table
            (cons 'defequal-table
                  (cons (cons 'quote (cons call 'nil))
                        (cons (cons 'quote (cons expansion 'nil))
                              'nil)))))))

Theorem: pseudo-event-formp-of-defequal-record-call

(defthm pseudo-event-formp-of-defequal-record-call
  (b* ((table-event (defequal-record-call call expansion)))
    (pseudo-event-formp table-event))
  :rule-classes :rewrite)