		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-table

Deftreeops-table-lookup

Look up a deftreeops in the table.

Signature
(deftreeops-table-lookup grammar wrld) → info?
Arguments: grammar — Guard (common-lisp::symbolp grammar).; wrld — Guard (plist-worldp wrld).
Returns: info? — Type (deftreeops-table-value-optionp info?).

Definitions and Theorems

Function: deftreeops-table-lookup

(defun deftreeops-table-lookup (grammar wrld)
  (declare (xargs :guard (and (common-lisp::symbolp grammar)
                              (plist-worldp wrld))))
  (let ((__function__ 'deftreeops-table-lookup))
    (declare (ignorable __function__))
    (b* ((info? (cdr (assoc-eq grammar
                               (table-alist+ 'deftreeops-table
                                             wrld)))))
      (and (deftreeops-table-valuep info?)
           info?))))

Theorem: deftreeops-table-value-optionp-of-deftreeops-table-lookup

(defthm deftreeops-table-value-optionp-of-deftreeops-table-lookup
  (b* ((info? (deftreeops-table-lookup grammar wrld)))
    (deftreeops-table-value-optionp info?))
  :rule-classes :rewrite)