		Search-engine friendly clone of the ACL2 documentation.

Transformation-table

Previous-transformation-expansion

Retrieve the encapsulate previously generated by this transformation call, if any.

Signature
(previous-transformation-expansion call wrld) → encapsulate?
Arguments: call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: encapsulate? — A pseudo-event-formp or nil.

The :print and :show-only inputs, if present, are removed from the call prior to looking it up in the transformation table. See the discussion here for motivation.

The encapsulate associated to the call is returned, if found; otherwise, nil is returned. Thus, a non-nil result means that the call is redundant.

Definitions and Theorems

Function: previous-transformation-expansion

(defun previous-transformation-expansion (call wrld)
 (declare (xargs :guard (and (pseudo-event-formp call)
                             (plist-worldp wrld))))
 (let ((__function__ 'previous-transformation-expansion))
  (declare (ignorable __function__))
  (b*
   ((table (table-alist 'transformation-table
                        wrld)
)
    (call
      (remove-irrelevant-inputs-from-transformation-call call wrld))
    (pair (assoc-equal call table)))
   (if pair (cdr pair) nil))))