Encode the name of an STV line, when the name is a list of E bits.
(stv-name-bits-to-xml bits col acc) → 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.
(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))))
(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)