AIJ's constants (i.e. static final fields) for certain ACL2 symbols.
This is an alist from the ACL2 symbols to the names of the corresponding fields.
Definition:
(defconst *aij-symbol-constants* '((t . "T") (nil . "NIL") (list . "LIST") (if . "IF") (characterp . "CHARACTERP") (stringp . "STRINGP") (symbolp . "SYMBOLP") (integerp . "INTEGERP") (rationalp . "RATIONALP") (complex-rationalp . "COMPLEX_RATIONALP") (acl2-numberp . "ACL2_NUMBERP") (consp . "CONSP") (char-code . "CHAR_CODE") (code-char . "CODE_CHAR") (coerce . "COERCE") (intern-in-package-of-symbol . "INTERN_IN_PACKAGE_OF_SYMBOL") (symbol-package-name . "SYMBOL_PACKAGE_NAME") (symbol-name . "SYMBOL_NAME") (pkg-imports . "PKG_IMPORTS") (pkg-witness . "PKG_WITNESS") (unary-- . "UNARY_MINUS") (unary-/ . "UNARY_SLASH") (binary-+ . "BINARY_PLUS") (binary-* . "BINARY_STAR") (< . "LESS_THAN") (complex . "COMPLEX") (realpart . "REALPART") (imagpart . "IMAGPART") (numerator . "NUMERATOR") (denominator . "DENOMINATOR") (cons . "CONS") (car . "CAR") (cdr . "CDR") (equal . "EQUAL") (bad-atom<= . "BAD_ATOM_LESS_THAN_OR_EQUAL_TO") (or . "OR") (nonnegative-integer-quotient . "NONNEGATIVE_INTEGER_QUOTIENT") (string-append . "STRING_APPEND") (len . "LEN") (char . "CHAR") (hard-error . "HARD_ERROR")))