		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-expand-input-entries

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

Signature
(stv-expand-input-entries name width pnum entries gensyms usersyms prev-val) → (mv new-entries gensyms usersyms)
Arguments: name — Guard (and (atom-listp name) (consp name)).; width — Guard (equal width (len name)).; pnum — Guard (natp pnum).; entries — Guard (true-listp entries).

Definitions and Theorems

Function: stv-expand-input-entries

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

Theorem: stv-expand-input-entries-mvtypes-0

(defthm stv-expand-input-entries-mvtypes-0
 (true-listp
  (mv-nth
      0
      (stv-expand-input-entries name width pnum
                                entries gensyms usersyms prev-val)))
 :rule-classes :type-prescription)

Theorem: true-listp-of-stv-expand-input-entries-gensyms

(defthm true-listp-of-stv-expand-input-entries-gensyms
 (implies
   (true-listp gensyms)
   (b*
    (((mv ?new-entries gensyms ?usersyms)
      (stv-expand-input-entries name width pnum
                                entries gensyms usersyms prev-val)))
    (true-listp gensyms))))