		Search-engine friendly clone of the ACL2 documentation.

Svtv-doc

Stv-lines-to-xml

Signature
(stv-lines-to-xml lines expansions acc) → acc
Arguments: lines — Guard (true-list-listp lines).; expansions — Guard (svtv-lines-p expansions).
Returns: acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: stv-lines-to-xml

(defun stv-lines-to-xml (lines expansions acc)
  (declare (xargs :guard (and (true-list-listp lines)
                              (svtv-lines-p expansions))))
  (let ((__function__ 'stv-lines-to-xml))
    (declare (ignorable __function__))
    (b* (((when (atom lines)) acc)
         ((cons expansion1 rest-expansions)
          (if (atom expansions)
              (cons nil nil)
            expansions))
         (acc (stv-line-to-xml (car lines)
                               expansion1 acc)))
      (stv-lines-to-xml (cdr lines)
                        rest-expansions acc))))

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

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