		Search-engine friendly clone of the ACL2 documentation.

Svtv-doc

Stv-entries-to-xml

Encode all the values from an STV line.

Signature
(stv-entries-to-xml entries expansions acc) → acc
Arguments: entries — The original entries for this line.; expansions — The expanded entries for this line.
Guard (svtv-entrylist-p expansions).
Returns: acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: stv-entries-to-xml

(defun stv-entries-to-xml (entries expansions acc)
  (declare (xargs :guard (svtv-entrylist-p expansions)))
  (let ((__function__ 'stv-entries-to-xml))
    (declare (ignorable __function__))
    (b* (((when (atom entries)) acc)
         (acc (str::revappend-chars "<stv_entry>" acc))
         (acc (stv-entry-to-xml (car entries)
                                (and (consp expansions)
                                     (car expansions))
                                acc))
         (acc (str::revappend-chars "</stv_entry>" acc)))
      (stv-entries-to-xml (cdr entries)
                          (and (consp expansions)
                               (cdr expansions))
                          acc))))

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

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