		Search-engine friendly clone of the ACL2 documentation.

Svtv-doc

Stv-repeat-last-entry

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

Definitions and Theorems

Function: stv-repeat-last-entry

(defun stv-repeat-last-entry (line nphases)
  (declare (xargs :guard (and (true-listp line) (natp nphases))))
  (let ((__function__ 'stv-repeat-last-entry))
    (declare (ignorable __function__))
    (b* ((line (list-fix line))
         (llen (len line))
         (nphases (+ 1 nphases))
         ((unless (<= llen nphases))
          (er hard? 'stv-repeat-last-entry
              "Number of phases is too small: line ~x0, nphases ~x1"
              line nphases))
         ((when (= llen nphases)) line)
         (last-entry (car (last line)))
         (new-tail (repeat (- nphases llen) last-entry)))
      (append line new-tail))))

Theorem: true-listp-of-stv-repeat-last-entry

(defthm true-listp-of-stv-repeat-last-entry
  (b* ((new-line (stv-repeat-last-entry line nphases)))
    (true-listp new-line))
  :rule-classes :rewrite)