		Search-engine friendly clone of the ACL2 documentation.

Defgrammar-table

Defgrammar-table-lookup

Look up a defgrammar call in the table.

Signature
(defgrammar-table-lookup call wrld) → yes/no
Arguments: call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

Returns a boolean, saying whether the call is in the table or not.

Definitions and Theorems

Function: defgrammar-table-lookup

(defun defgrammar-table-lookup (call wrld)
  (declare (xargs :guard (and (pseudo-event-formp call)
                              (plist-worldp wrld))))
  (let ((__function__ 'defgrammar-table-lookup))
    (declare (ignorable __function__))
    (consp (assoc-equal call
                        (table-alist+ 'defgrammar-table
                                      wrld)))))

Theorem: booleanp-of-defgrammar-table-lookup

(defthm booleanp-of-defgrammar-table-lookup
  (b* ((yes/no (defgrammar-table-lookup call wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)