verbosep - ACL2 Book

other

(in-package "XDOC")

other

(defstub xdoc-verbose-p nil t)

xdoc-verbose-fnfunction

(defun xdoc-verbose-fn
  nil
  (declare (xargs :guard t))
  t)

xdoc-quiet-fnfunction

(defun xdoc-quiet-fn
  nil
  (declare (xargs :guard t))
  nil)

xdoc-verbosemacro

(defmacro xdoc-verbose
  nil
  `(defattach xdoc-verbose-p xdoc-verbose-fn))

xdoc-quietmacro

(defmacro xdoc-quiet
  nil
  `(defattach xdoc-verbose-p xdoc-quiet-fn))

other

(xdoc-verbose)