		Search-engine friendly clone of the ACL2 documentation.

Stv-doc

Stv-name-bits-to-xml

Encode the name of an STV line, when the name is a list of E bits.

Signature
(stv-name-bits-to-xml bits col acc) → acc
Arguments: bits — Guard (true-listp bits).; col — Guard (natp col).
Returns: acc — Type (character-listp acc), given (character-listp acc).

This is really horrible, but it doesn't matter since nobody would ever actually use a list of E bits to name their input.

Definitions and Theorems

Function: stv-name-bits-to-xml

(defun stv-name-bits-to-xml (bits col acc)
  (declare (xargs :guard (and (true-listp bits) (natp col))))
  (let ((__function__ 'stv-name-bits-to-xml))
    (declare (ignorable __function__))
    (b* (((when (atom bits)) acc)
         (name1 (stringify (car bits)))
         ((mv col acc)
          (vl2014::vl-html-encode-string-aux name1 0 (length name1)
                                             (lnfix col)
                                             8 acc))
         ((mv col acc)
          (if (atom (cdr bits))
              (mv col acc)
            (mv (+ col 2)
                (list* #\Space #\, acc)))))
      (stv-name-bits-to-xml (cdr bits)
                            col acc))))

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

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