• Top
    • Documentation
      • Xdoc
        • Undocumented
        • Save
        • Defsection
        • Markup
        • Preprocessor
        • Emacs-links
        • Defxdoc
        • Katex-integration
        • Constructors
          • Primitive-constructors
          • Composite-constructors
            • Xdoc::apt-constructors
            • Generic-composite-constructors
              • Desc
              • Codeblock
              • Seetopic
              • Ahref
              • Topstring
                • Topstring-@def
                • Topstring-p
              • Event-macro-xdoc-constructors
            • Constructor-preliminaries
            • Trees
          • Entities
          • Save-rendered
          • Add-resource-directory
          • Defxdoc+
          • Testing
          • Order-subtopics
          • Missing-parents
          • Save-rendered-event
          • Archive-matching-topics
          • 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
      • Debugging
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Generic-composite-constructors

    Topstring

    Construct an XDOC string from a sequence of XDOC trees.

    This can be used to construct XDOC strings at the ``top level'', e.g. :short and :long documentation string.

    Macro: topstring

    (defmacro topstring (&rest trees)
              (cons 'tree-to-string
                    (cons (cons '&& trees) 'nil)))