		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-safe-next-n

Used to get a context for error messages.

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

Definitions and Theorems

Function: vl-safe-next-n

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

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

(defthm vl-echarlist-p-of-vl-safe-next-n
  (implies (vl-echarlist-p remainder)
           (b* ((next-n (vl-safe-next-n n remainder)))
             (vl-echarlist-p next-n)))
  :rule-classes :rewrite)