		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)