		Search-engine friendly clone of the ACL2 documentation.

Primitive-constructors

Blockquote

Construct an XDOC tree for an HTML quoted block <blockquote>...</blockquote>.

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

Macro: blockquote

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

Definitions and Theorems

Function: blockquote-fn

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

Theorem: stringp-of-blockquote

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