• Top
    • Documentation
      • Xdoc
        • Undocumented
        • Save
        • Defsection
        • Markup
        • Preprocessor
        • Terminal
        • Emacs-links
        • Defxdoc
        • Katex-integration
        • Constructors
          • Primitive-constructors
          • Composite-constructors
          • Constructor-preliminaries
            • Partition-macro-args
            • String-downcase$
            • Keyword-macro-args-to-terms
            • String-escape
            • *newline*
          • Trees
        • Entities
        • Defxdoc+
        • Save-rendered
        • Add-resource-directory
        • Testing
        • Order-subtopics
        • Save-rendered-event
        • Archive-matching-topics
        • Archive-xdoc
        • Xdoc-extend
        • Set-default-parents
        • Missing-parents
        • Defpointer
        • Defxdoc-raw
        • Xdoc-tests
        • Xdoc-prepend
        • Defsection-progn
        • Gen-xdoc-for-file
      • ACL2-doc
      • Recursion-and-induction
      • Loop$-primer
      • Operational-semantics
      • Pointers
      • Doc
      • Documentation-copyright
      • Course-materials
      • Args
      • ACL2-doc-summary
      • Finding-documentation
      • Broken-link
      • Doc-terminal-test-2
      • Doc-terminal-test-1
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Constructors

Constructor-preliminaries

Some preliminary utilities used by the XDOC constructors.

These are independent from the XDOC constructors, but we introduce them here to keep the XDOC constructor utilities self-contained.

Subtopics

Partition-macro-args
Partition the arguments of a macro into a list and an alist.
String-downcase$
A variant of common-lisp::string-downcase applicable to any string.
Keyword-macro-args-to-terms
Turn the keyword arguments of a macro into terms.
String-escape
Escape certain characters in a string, using backslashes.
*newline*
The string consisting of exactly the newline character.