(code-in-charset-p code set) determines if the character whose code is
code is a member of the character set set.
(code-in-charset-p code set) → *
- set — Guard (charset-p set).
Typically there's no reason to use this. But if you already have
the character code available for some reason, this may be slightly more
efficient than turning it back into a character and then calling char-in-charset-p.
Definitions and Theorems
(defun code-in-charset-p$inline (code set)
(declare (type (unsigned-byte 8) code))
(declare (xargs :guard (charset-p set)))
(let ((acl2::__function__ 'code-in-charset-p))
(declare (ignorable acl2::__function__))
(mbe :logic (char-in-charset-p (code-char code) set)
:exec (logbitp code set))))