		Search-engine friendly clone of the ACL2 documentation.

Stv-doc

Stv-name-to-xml

Encode the name of an STV line.

Signature
(stv-name-to-xml name acc) → acc
Returns: acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: stv-name-to-xml

(defun stv-name-to-xml (name acc)
 (declare (xargs :guard t))
 (let ((__function__ 'stv-name-to-xml))
  (declare (ignorable __function__))
  (cond
      ((stringp name)
       (b* (((mv ?col acc)
             (vl2014::vl-html-encode-string-aux name 0 (length name)
                                                0 8 acc)))
         acc))
      ((true-listp name)
       (b* ((acc (cons #\{ acc))
            (acc (stv-name-bits-to-xml name 1 acc))
            (acc (cons #\} acc)))
         acc))
      (t (raise "Bad name for stv line: ~x0." name)))))

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

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