		Search-engine friendly clone of the ACL2 documentation.

Printable-chars

A character set for printable-char-p.

Function: printable-chars$inline

(defun printable-chars$inline nil
  (declare (xargs :guard t))
  170141183460469231731687303711589138432)

Theorem: charset-p-of-printable-chars

(defthm charset-p-of-printable-chars
  (charset-p (printable-chars)))

Theorem: char-in-charset-p-of-printable-chars

(defthm char-in-charset-p-of-printable-chars
  (equal (char-in-charset-p x (printable-chars))
         (printable-char-p x)))