• Top
  • Documentation
    • Xdoc
      • Undocumented
      • Save
      • Defsection
      • Markup
      • Preprocessor
      • Emacs-links
      • Defxdoc
      • Katex-integration
      • Constructors
        • Primitive-constructors
        • Composite-constructors
        • Constructor-preliminaries
        • Trees
          • Tree-to-string
          • Treep
          • Make-tree-dir/&&
          • Make-tree-tag
      • Entities
      • Save-rendered
      • Add-resource-directory
      • Defxdoc+
      • Testing
      • Order-subtopics
      • Save-rendered-event
      • Archive-matching-topics
      • Missing-parents
      • Archive-xdoc
      • Xdoc-extend
      • Set-default-parents
      • Defpointer
      • Defxdoc-raw
      • Xdoc-tests
      • Xdoc-prepend
      • Defsection-progn
      • Gen-xdoc-for-file
    • ACL2-doc
    • Pointers
    • Doc
    • Documentation-copyright
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Trees

Make-tree-dir/&&

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.

Definitions and Theorems

Function: make-tree-dir/&&

(defun make-tree-dir/&& (dir/&& trees)
       (declare (xargs :guard (and (keywordp dir/&&)
                                   (tree-listp trees))))
       (cons dir/&& trees))

Theorem: treep-of-make-tree-dir/&&

(defthm treep-of-make-tree-dir/&&
        (implies (keywordp dir/&&)
                 (equal (treep (make-tree-dir/&& dir/&& trees))
                        (tree-listp trees))))