		Search-engine friendly clone of the ACL2 documentation.

Svtv-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__))
    (b* (((when (stringp name))
          (b* (((mv ?col acc)
                (str::html-encode-string-aux name 0 (length name)
                                             0 8 acc)))
            acc))
         (str (str::pretty name))
         ((mv ?col acc)
          (str::html-encode-string-aux str 0 (length str)
                                       0 8 acc)))
      acc)))

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)