Construct a non-leaf XDOC tree with a preprocessor directive or a tree concatenation at the root.
This is for internal use of the XDOC constructor library. Users of this library should use the constructor && for concatenation or constructors for specific directives, e.g. @def.
See also make-tree-tag.
Function:
(defun make-tree-dir/&& (dir/&& trees) (declare (xargs :guard (and (keywordp dir/&&) (tree-listp trees)))) (cons dir/&& trees))
Theorem:
(defthm treep-of-make-tree-dir/&& (implies (keywordp dir/&&) (equal (treep (make-tree-dir/&& dir/&& trees)) (tree-listp trees))))