(code-in-charset-p code set) determines if the character whose code is
(code-in-charset-p code 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.
(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))))