		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))))