		Search-engine friendly clone of the ACL2 documentation.

Stv-expand

Stv-expand-names-in-lines

Expands all of the names in a list of STV :input or :output lines.

Signature
(stv-expand-names-in-lines lines type mod) → new-lines
Arguments: lines — Guard (true-list-listp lines).; type — Guard (or (eq type :i) (eq type :o)).

Definitions and Theorems

Function: stv-expand-names-in-lines

(defun stv-expand-names-in-lines
       (lines type mod)
       (declare (xargs :guard (and (true-list-listp lines)
                                   (or (eq type :i) (eq type :o)))))
       (let ((__function__ 'stv-expand-names-in-lines))
            (declare (ignorable __function__))
            (b* (((when (atom lines)) nil)
                 (line1 (car lines))
                 ((cons name phases) line1)
                 (new-name (stv-expand-name name type mod)))
                (cons (cons new-name phases)
                      (stv-expand-names-in-lines (cdr lines)
                                                 type mod)))))

Theorem: alistp-of-stv-expand-names-in-lines

(defthm alistp-of-stv-expand-names-in-lines
        (alistp (stv-expand-names-in-lines lines type mod)))

Theorem: true-list-listp-of-stv-expand-names-in-lines

(defthm
 true-list-listp-of-stv-expand-names-in-lines
 (implies
      (true-list-listp lines)
      (true-list-listp (stv-expand-names-in-lines lines type mod))))