		Search-engine friendly clone of the ACL2 documentation.

Stv-doc

Stv-lines-to-xml

Signature
(stv-lines-to-xml lines expansions acc) → acc
Arguments: lines — Guard (true-list-listp lines).; expansions — Guard (true-list-listp 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)
                              (true-list-listp expansions))))
  (let ((__function__ 'stv-lines-to-xml))
    (declare (ignorable __function__))
    (b* (((when (atom lines)) acc)
         (acc (stv-line-to-xml (car lines)
                               (car expansions)
                               acc)))
      (stv-lines-to-xml (cdr lines)
                        (cdr 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)