Look up a deftreeops call in the table.
(deftreeops-table-lookup call wrld) → info?
Returns a boolean, saying whether the call is in the table or not.
Function:
(defun deftreeops-table-lookup (call wrld) (declare (xargs :guard (and (pseudo-event-formp call) (plist-worldp wrld)))) (let ((__function__ 'deftreeops-table-lookup)) (declare (ignorable __function__)) (b* ((info? (cdr (assoc-equal call (table-alist+ 'deftreeops-table wrld))))) (and (deftreeops-table-valuep info?) info?))))
Theorem:
(defthm deftreeops-table-value-optionp-of-deftreeops-table-lookup (b* ((info? (deftreeops-table-lookup call wrld))) (deftreeops-table-value-optionp info?)) :rule-classes :rewrite)