Compute the total length of the list, in characters.
(vl-printedlist-length x acc) → len
This is different than ordinary len because any strings within the list may have their own lengths.
Function:
(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:
(defthm natp-of-vl-printedlist-length (b* ((len (vl-printedlist-length x acc))) (natp len)) :rule-classes :type-prescription)