		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-expand-internal-lines

Extend stv-expand-internal-line across a list of lines.

Signature
(stv-expand-internal-lines lines usersyms mod) → (mv new-lines usersyms)
Arguments: lines — Guard (true-list-listp lines).; mod — Guard (good-esim-modulep mod).
Returns: new-lines — Type (true-list-listp new-lines).

Definitions and Theorems

Function: stv-expand-internal-lines

(defun stv-expand-internal-lines (lines usersyms mod)
  (declare (xargs :guard (and (true-list-listp lines)
                              (good-esim-modulep mod))))
  (let ((__function__ 'stv-expand-internal-lines))
    (declare (ignorable __function__))
    (b* (((when (atom lines)) (mv nil usersyms))
         ((mv line1 usersyms)
          (stv-expand-internal-line (car lines)
                                    usersyms mod))
         ((mv lines2 usersyms)
          (stv-expand-internal-lines (cdr lines)
                                     usersyms mod)))
      (mv (cons line1 lines2) usersyms))))

Theorem: true-list-listp-of-stv-expand-internal-lines.new-lines

(defthm true-list-listp-of-stv-expand-internal-lines.new-lines
  (b* (((mv ?new-lines ?usersyms)
        (stv-expand-internal-lines lines usersyms mod)))
    (true-list-listp new-lines))
  :rule-classes :rewrite)