		Search-engine friendly clone of the ACL2 documentation.

Printconfig

Printconfig->print-lowercase

Get the print-lowercase field from a printconfig.

Signature
(printconfig->print-lowercase x) → print-lowercase
Arguments: x — Guard (printconfig-p x).
Returns: print-lowercase — Type (booleanp print-lowercase).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: printconfig->print-lowercase$inline

(defun printconfig->print-lowercase$inline (x)
 (declare (xargs :guard (printconfig-p x)))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'printconfig->print-lowercase))
  (declare (ignorable acl2::__function__))
  (mbe
    :logic
    (b* ((x (and t x)))
      (acl2::bool-fix
           (std::prod-cdr (std::prod-cdr (std::prod-cdr (cdr x))))))
    :exec (std::prod-cdr (std::prod-cdr (std::prod-cdr (cdr x)))))))

Theorem: booleanp-of-printconfig->print-lowercase

(defthm booleanp-of-printconfig->print-lowercase
  (b* ((print-lowercase (printconfig->print-lowercase$inline x)))
    (booleanp print-lowercase))
  :rule-classes :type-prescription)

Theorem: printconfig->print-lowercase$inline-of-printconfig-fix-x

(defthm printconfig->print-lowercase$inline-of-printconfig-fix-x
  (equal (printconfig->print-lowercase$inline (printconfig-fix x))
         (printconfig->print-lowercase$inline x)))

Theorem: printconfig->print-lowercase$inline-printconfig-equiv-congruence-on-x

(defthm
 printconfig->print-lowercase$inline-printconfig-equiv-congruence-on-x
 (implies (printconfig-equiv x x-equiv)
          (equal (printconfig->print-lowercase$inline x)
                 (printconfig->print-lowercase$inline x-equiv)))
 :rule-classes :congruence)