		Search-engine friendly clone of the ACL2 documentation.

Trees

Make-tree-tag

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.

Definitions and Theorems

Function: make-tree-tag

(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: treep-of-make-tree-tag

(defthm treep-of-make-tree-tag
        (equal (treep (make-tree-tag tag attributes trees))
               (and (keywordp tag)
                    (keyword-tree-alistp attributes)
                    (tree-listp trees))))