		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Pinst->width

Signature
(pinst->width x) → width
Arguments: x — Guard (pinst-p x).
Returns: width — Type (posp width).

Definitions and Theorems

Function: pinst->width

(defun pinst->width (x)
  (declare (xargs :guard (pinst-p x)))
  (let ((acl2::__function__ 'pinst->width))
    (declare (ignorable acl2::__function__))
    (pinst-case x
                :flat (pflat->width x.guts)
                :keyline (pflat->width x.guts)
                :dot x.width
                :quote x.width
                :wide x.width
                :keypair x.width
                :indent x.width
                :special-term x.width)))

Theorem: posp-of-pinst->width

(defthm posp-of-pinst->width
  (b* ((width (pinst->width x)))
    (posp width))
  :rule-classes :type-prescription)