		Search-engine friendly clone of the ACL2 documentation.

Charset-p

Char-in-charset-p

(char-in-charset-p char set) determines if the character char is a member of the character set set.

Signature
(char-in-charset-p char set) → *
Arguments: set — Guard (charset-p set).

Definitions and Theorems

Function: char-in-charset-p$inline

(defun
   char-in-charset-p$inline (char set)
   (declare (type character char))
   (declare (xargs :guard (charset-p set)))
   (let ((acl2::__function__ 'char-in-charset-p))
        (declare (ignorable acl2::__function__))
        (mbe :logic (and (characterp char)
                         (logbitp (char-code char) set))
             :exec (logbitp (the (unsigned-byte 8) (char-code char))
                            set))))

Theorem: char-in-charset-p-when-not-character

(defthm char-in-charset-p-when-not-character
        (implies (not (characterp char))
                 (not (char-in-charset-p char set))))