Construct a non-leaf XDOC tree with an XML tag at the root.
This is for internal use of the XDOC constructor library. Users of this library should use constructors for specific tags, e.g. p.
See also make-tree-dir/&&.
Function:
(defun make-tree-tag (tag attributes trees) (declare (xargs :guard (and (keywordp tag) (keyword-tree-alistp attributes) (tree-listp trees)))) (cons (cons tag attributes) trees))
Theorem:
(defthm treep-of-make-tree-tag (equal (treep (make-tree-tag tag attributes trees)) (and (keywordp tag) (keyword-tree-alistp attributes) (tree-listp trees))))