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