Event to update the table of atc calls.
(atc-table-record-event call info) → event
Function:
(defun atc-table-record-event (call info) (declare (xargs :guard (and (pseudo-event-formp call) (atc-call-infop info)))) (let ((__function__ 'atc-table-record-event)) (declare (ignorable __function__)) (cons 'table (cons *atc-table* (cons (cons 'quote (cons call 'nil)) (cons (cons 'quote (cons info 'nil)) 'nil))))))
Theorem:
(defthm pseudo-event-formp-of-atc-table-record-event (b* ((event (atc-table-record-event call info))) (pseudo-event-formp event)) :rule-classes :rewrite)