		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-expand-output-entries

Extend stv-expand-output-entry across a line.

Signature
(stv-expand-output-entries name width pnum entries usersyms) → (mv new-entries usersyms)
Arguments: name — Guard (and (true-listp name) (consp name)).; width — Guard (equal width (len name)).; pnum — Guard (natp pnum).; entries — Guard (true-listp entries).
Returns: new-entries — Type (true-listp new-entries).

Definitions and Theorems

Function: stv-expand-output-entries

(defun
   stv-expand-output-entries
   (name width pnum entries usersyms)
   (declare (xargs :guard (and (and (true-listp name) (consp name))
                               (natp pnum)
                               (true-listp entries)
                               (equal width (len name)))))
   (let ((__function__ 'stv-expand-output-entries))
        (declare (ignorable __function__))
        (b* (((when (atom entries))
              (mv nil usersyms))
             ((mv new-car usersyms)
              (stv-expand-output-entry name width pnum (car entries)
                                       usersyms))
             ((mv new-cdr usersyms)
              (stv-expand-output-entries name width (+ 1 pnum)
                                         (cdr entries)
                                         usersyms)))
            (mv (cons new-car new-cdr) usersyms))))

Theorem: true-listp-of-stv-expand-output-entries.new-entries

(defthm
 true-listp-of-stv-expand-output-entries.new-entries
 (b*
    (((mv ?new-entries ?usersyms)
      (stv-expand-output-entries name width pnum entries usersyms)))
    (true-listp new-entries))
 :rule-classes :type-prescription)