• Top
    • Documentation
      • Xdoc
        • Undocumented
        • Save
        • Defsection
        • Markup
        • Preprocessor
        • Emacs-links
        • Defxdoc
        • Katex-integration
        • Constructors
          • Primitive-constructors
            • Generate-primitive-constructor-for-tag
            • Generate-primitive-constructor-for-dir/&&
            • Code
            • Ul
            • Tt
            • P
            • Blockquote
            • Th
            • Table_
            • Sf
            • See_
            • Ol
            • Li
            • Img
            • H5
            • H4
            • H3
            • H2
            • H1
            • Dl
            • Color
            • A
              • U_
              • Tr
              • Td
              • I
              • Dt
              • Dd
              • Br
              • Box
              • B
              • @def
              • @{}
              • &&
              • @[]
              • @''
              • @$$
              • @``
              • @url
              • @tsee
              • @sym
              • @srclink
              • @see?
              • @see
              • @measure
              • @gdef
              • @formals
              • @csym
              • @csee
              • @call
              • @body
            • Composite-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
    • Primitive-constructors

    A

    Construct an XDOC tree for an HTML hyperlink <a>...</a>.

    See the primitive constructors topic for information about the kind of arguments that must be passed to this constructor.

    Macro: a

    (defmacro
       a (&rest args)
       (mv-let
            (trees attributes)
            (partition-macro-args args 'a)
            (let ((attributes (keyword-macro-args-to-terms attributes)))
                 (list 'a-fn
                       (cons 'list attributes)
                       (cons 'list trees)))))

    Definitions and Theorems

    Function: a-fn

    (defun a-fn (attributes trees)
           (declare (xargs :guard (and (keyword-tree-alistp attributes)
                                       (tree-listp trees))))
           (make-tree-tag :a attributes trees))

    Theorem: stringp-of-a

    (defthm stringp-of-a
            (equal (treep (a-fn attributes trees))
                   (and (keyword-tree-alistp attributes)
                        (tree-listp trees))))