		Search-engine friendly clone of the ACL2 documentation.

&&

Construct an XDOC tree for a concatenation.

Macro: &&

(defmacro && (&rest trees)
  (list '&&-fn (cons 'list trees)))

Function: &&-fn

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

Theorem: stringp-of-&&

(defthm stringp-of-&&
  (equal (treep (&&-fn trees))
         (tree-listp trees)))