		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-table

Defdefparse-table-lookup

Look up a defdefparse call in the table.

Signature
(defdefparse-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: defdefparse-table-lookup

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

Theorem: booleanp-of-defdefparse-table-lookup

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