		Search-engine friendly clone of the ACL2 documentation.

Vl-printedlist-p

Vl-printedlist-length

Compute the total length of the list, in characters.

Signature
(vl-printedlist-length x acc) → len
Arguments: x — Guard (vl-printedlist-p x).; acc — Guard (natp acc).
Returns: len — Type (natp len).

This is different than ordinary len because any strings within the list may have their own lengths.

Definitions and Theorems

Function: vl-printedlist-length

(defun vl-printedlist-length (x acc)
  (declare (xargs :guard (and (vl-printedlist-p x) (natp acc))))
  (let ((__function__ 'vl-printedlist-length))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (lnfix acc))
         (x1 (vl-printed-fix (car x)))
         (len1 (if (characterp x1) 1 (length x1))))
      (vl-printedlist-length (cdr x)
                             (+ len1 (lnfix acc))))))

Theorem: natp-of-vl-printedlist-length

(defthm natp-of-vl-printedlist-length
  (b* ((len (vl-printedlist-length x acc)))
    (natp len))
  :rule-classes :type-prescription)