		Search-engine friendly clone of the ACL2 documentation.

@see?

Construct an XDOC tree for a conditional topic link directive @(see? ...).

Macro: @see?

(defmacro @see? (&rest trees)
  (list '@see?-fn (cons 'list trees)))

Function: @see?-fn

(defun @see?-fn (trees)
  (declare (xargs :guard (tree-listp trees)))
  (make-tree-dir/&& :@see? trees))

Theorem: stringp-of-@see?

(defthm stringp-of-@see?
  (equal (treep (@see?-fn trees))
         (tree-listp trees)))