		Search-engine friendly clone of the ACL2 documentation.

Defgrammar-table

Defgrammar-table-add

Event to record a defgrammar call in the table.

Signature
(defgrammar-table-add call) → event
Arguments: call — Guard (pseudo-event-formp call).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: defgrammar-table-add

(defun defgrammar-table-add (call)
  (declare (xargs :guard (pseudo-event-formp call)))
  (let ((__function__ 'defgrammar-table-add))
    (declare (ignorable __function__))
    (cons 'table
          (cons 'defgrammar-table
                (cons (cons 'quote (cons call 'nil))
                      '(nil))))))

Theorem: pseudo-event-formp-of-defgrammar-table-add

(defthm pseudo-event-formp-of-defgrammar-table-add
  (b* ((event (defgrammar-table-add call)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)