		Search-engine friendly clone of the ACL2 documentation.

Stv-doc

Stv-labels-to-xml

Signature
(stv-labels-to-xml labels acc) → acc
Arguments: labels — Guard (symbol-listp labels).
Returns: acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: stv-labels-to-xml

(defun stv-labels-to-xml (labels acc)
  (declare (xargs :guard (symbol-listp labels)))
  (let ((__function__ 'stv-labels-to-xml))
    (declare (ignorable __function__))
    (b* (((when (atom labels)) acc)
         (acc (str::revappend-chars "<stv_label>" acc))
         (acc (if (car labels)
                  (str::revappend-chars (symbol-name (car labels))
                                        acc)
                acc))
         (acc (str::revappend-chars "</stv_label>" acc)))
      (stv-labels-to-xml (cdr labels) acc))))

Theorem: character-listp-of-stv-labels-to-xml

(defthm character-listp-of-stv-labels-to-xml
  (implies (character-listp acc)
           (b* ((acc (stv-labels-to-xml labels acc)))
             (character-listp acc)))
  :rule-classes :rewrite)