		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-safe-previous-n

Used to get a context for error messages.

Signature
(vl-safe-previous-n n acc) → prev-n
Arguments: n — Guard (natp n).
Returns: prev-n — Type (vl-echarlist-p prev-n), given (vl-echarlist-p acc).

Definitions and Theorems

Function: vl-safe-previous-n

(defun vl-safe-previous-n (n acc)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'vl-safe-previous-n))
    (declare (ignorable __function__))
    (reverse (first-n (min (nfix n) (len acc))
                      acc))))

Theorem: vl-echarlist-p-of-vl-safe-previous-n

(defthm vl-echarlist-p-of-vl-safe-previous-n
  (implies (vl-echarlist-p acc)
           (b* ((prev-n (vl-safe-previous-n n acc)))
             (vl-echarlist-p prev-n)))
  :rule-classes :rewrite)