		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-table

Deftreeops-table-add

Event to record a deftreeops in the table.

Signature
(deftreeops-table-add grammar info) → event
Arguments: grammar — Guard (common-lisp::symbolp grammar).; info — Guard (deftreeops-table-valuep info).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: deftreeops-table-add

(defun deftreeops-table-add (grammar info)
  (declare (xargs :guard (and (common-lisp::symbolp grammar)
                              (deftreeops-table-valuep info))))
  (let ((__function__ 'deftreeops-table-add))
    (declare (ignorable __function__))
    (cons 'table
          (cons 'deftreeops-table
                (cons (cons 'quote (cons grammar 'nil))
                      (cons (cons 'quote (cons info 'nil))
                            'nil))))))

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

(defthm pseudo-event-formp-of-deftreeops-table-add
  (b* ((event (deftreeops-table-add grammar info)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)