		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Pinstlist->max-width

Signature
(pinstlist->max-width x maximum) → maximum
Arguments: x — Guard (pinstlist-p x).; maximum — Guard (integerp maximum).
Returns: maximum — Type (integerp maximum).

Definitions and Theorems

Function: pinstlist->max-width

(defun pinstlist->max-width (x maximum)
  (declare (xargs :guard (and (pinstlist-p x)
                              (integerp maximum))))
  (let ((acl2::__function__ 'pinstlist->max-width))
    (declare (ignorable acl2::__function__))
    (b* (((when (atom x)) (acl2::lifix maximum))
         (width1 (pinst->width (car x)))
         ((when (> width1 maximum))
          (pinstlist->max-width (cdr x) width1)))
      (pinstlist->max-width (cdr x)
                            maximum))))

Theorem: integerp-of-pinstlist->max-width

(defthm integerp-of-pinstlist->max-width
  (b* ((maximum (pinstlist->max-width x maximum)))
    (integerp maximum))
  :rule-classes :type-prescription)