CHAR-CODE

the numeric code for a given character 
Major Section:  ACL2-BUILT-INS

Completion Axiom (completion-of-char-code): 

(equal (char-code x)
       (if (characterp x)
           (char-code x)
         0))

Guard for (char-code x): 

(characterp x)
This function maps all non-characters to 0.