		Search-engine friendly clone of the ACL2 documentation.

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))))