Major Section: ACL2-BUILT-INS
Non-characters in the given list are coerced to the character with code 0.
To see the ACL2 definition of this function, see pf.
