Create an event form to record a transformation call into the transformation table.
(record-transformation-call-event call encapsulate wrld) → event
The
Function:
(defun record-transformation-call-event (call encapsulate wrld) (declare (xargs :guard (and (pseudo-event-formp call) (pseudo-event-formp encapsulate) (plist-worldp wrld)))) (let ((__function__ 'record-transformation-call-event)) (declare (ignorable __function__)) (b* ((call (remove-irrelevant-inputs-from-transformation-call call wrld))) (cons 'table (cons 'transformation-table (cons (cons 'quote (cons call 'nil)) (cons (cons 'quote (cons encapsulate 'nil)) 'nil)))))))
Theorem:
(defthm pseudo-event-formp-of-record-transformation-call-event (b* ((event (record-transformation-call-event call encapsulate wrld))) (pseudo-event-formp event)) :rule-classes :rewrite)