		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)