		Search-engine friendly clone of the ACL2 documentation.

Printconfig

Printconfig-p

Recognizer for printconfig structures.

Signature
(printconfig-p x) → *

Definitions and Theorems

Function: printconfig-p

(defun printconfig-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'printconfig-p))
  (declare (ignorable acl2::__function__))
  (and
    (consp x)
    (eq (car x) :printconfig)
    (std::prod-consp (cdr x))
    (std::prod-consp (std::prod-car (cdr x)))
    (std::prod-consp (std::prod-cdr (std::prod-car (cdr x))))
    (std::prod-consp (std::prod-cdr (cdr x)))
    (std::prod-consp (std::prod-cdr (std::prod-cdr (cdr x))))
    (b*
     ((flat-right-margin (std::prod-car (std::prod-car (cdr x))))
      (hard-right-margin
           (std::prod-car (std::prod-cdr (std::prod-car (cdr x)))))
      (print-base
           (std::prod-cdr (std::prod-cdr (std::prod-car (cdr x)))))
      (print-radix (std::prod-car (std::prod-cdr (cdr x))))
      (home-package
           (std::prod-car (std::prod-cdr (std::prod-cdr (cdr x)))))
      (print-lowercase
           (std::prod-cdr (std::prod-cdr (std::prod-cdr (cdr x))))))
     (and (posp flat-right-margin)
          (posp hard-right-margin)
          (print-base-p print-base)
          (booleanp print-radix)
          (symbolp home-package)
          (booleanp print-lowercase))))))

Theorem: consp-when-printconfig-p

(defthm consp-when-printconfig-p
  (implies (printconfig-p x) (consp x))
  :rule-classes :compound-recognizer)