		Search-engine friendly clone of the ACL2 documentation.

Svtv-doc

Stv-repeat-last-entries

Signature
(stv-repeat-last-entries lines nphases) → new-lines
Arguments: lines — Guard (true-list-listp lines).; nphases — Guard (natp nphases).
Returns: new-lines — Type (true-list-listp new-lines).

Definitions and Theorems

Function: stv-repeat-last-entries

(defun stv-repeat-last-entries (lines nphases)
  (declare (xargs :guard (and (true-list-listp lines)
                              (natp nphases))))
  (let ((__function__ 'stv-repeat-last-entries))
    (declare (ignorable __function__))
    (if (atom lines)
        nil
      (cons (stv-repeat-last-entry (car lines)
                                   nphases)
            (stv-repeat-last-entries (cdr lines)
                                     nphases)))))

Theorem: true-list-listp-of-stv-repeat-last-entries

(defthm true-list-listp-of-stv-repeat-last-entries
  (b* ((new-lines (stv-repeat-last-entries lines nphases)))
    (true-list-listp new-lines))
  :rule-classes :rewrite)