Major Section: ACL2-BUILT-INS
(characterp x) is true if and only if x is a character.
(characterp x)
x