		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-expand-output-lines

Extend stv-expand-output-entry across a list of lines.

Signature
(stv-expand-output-lines lines usersyms) → (mv new-lines usersyms)
Arguments: lines — Guard (true-list-listp lines).
Returns: new-lines — Type (true-list-listp new-lines).

Definitions and Theorems

Function: stv-expand-output-lines

(defun
 stv-expand-output-lines (lines usersyms)
 (declare (xargs :guard (true-list-listp lines)))
 (let
  ((__function__ 'stv-expand-output-lines))
  (declare (ignorable __function__))
  (b*
   (((when (atom lines)) (mv nil usersyms))
    (line1 (car lines))
    ((cons name1 entries1) line1)
    ((unless (and (consp name1) (atom-listp name1)))
     (raise
      "Expected :output line names to be already expanded to ~
                non-empty lists of E bits, but found ~x0."
      name1)
     (mv nil usersyms))
    ((mv new-entries1 usersyms)
     (stv-expand-output-entries name1 (len name1)
                                0 entries1 usersyms))
    (new-car (cons name1 new-entries1))
    ((mv new-cdr usersyms)
     (stv-expand-output-lines (cdr lines)
                              usersyms)))
   (mv (cons new-car new-cdr) usersyms))))

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

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