		Search-engine friendly clone of the ACL2 documentation.

Deftreeops

Deftreeops-show-info

Show the information from the deftreeops table associated to a given grammar constant name.

If there is no information in the table for the given grammar constant name, we print a message saying so.

Macro: deftreeops-show-info

(defmacro deftreeops-show-info (grammar)
  (declare (xargs :guard (common-lisp::symbolp grammar)))
  (cons 'make-event-terse
        (cons (cons 'deftreeops-show-info-fn
                    (cons (cons 'quote (cons grammar 'nil))
                          '((w state))))
              'nil)))

Definitions and Theorems

Function: deftreeops-show-info-fn

(defun deftreeops-show-info-fn (grammar wrld)
  (declare (xargs :guard (and (common-lisp::symbolp grammar)
                              (plist-worldp wrld))))
  (let ((__function__ 'deftreeops-show-info-fn))
    (declare (ignorable __function__))
    (b* ((info (deftreeops-table-lookup grammar wrld))
         ((unless info)
          (cw "~%No entry in DEFTREEOPS table for grammar ~x0.~%"
              grammar)
          '(value-triple :invisible))
         (- (cw "~%~x0.~%" info)))
      '(value-triple :invisible))))

Theorem: pseudo-event-formp-of-deftreeops-show-info-fn

(defthm pseudo-event-formp-of-deftreeops-show-info-fn
  (b* ((event (deftreeops-show-info-fn grammar wrld)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)