		Search-engine friendly clone of the ACL2 documentation.

Aij-notions

aij-symbol-constants

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: *aij-symbol-constants*

(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")))