		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitives

atj-jprim-conv-fns

List of (the names of) the ACL2 functions that model Java primitive conversions.

These are all the conversions between primitive types.

Definition: *atj-jprim-conv-fns*

(defconst *atj-jprim-conv-fns*
  '(byte-to-short byte-to-int byte-to-long byte-to-float
                  byte-to-double short-to-int
                  short-to-long short-to-float
                  short-to-double char-to-int char-to-long
                  char-to-float char-to-double
                  int-to-long int-to-float int-to-double
                  long-to-float long-to-double
                  float-to-double short-to-byte
                  short-to-char char-to-byte char-to-short
                  int-to-byte int-to-short int-to-char
                  long-to-byte long-to-short long-to-char
                  long-to-int float-to-byte float-to-short
                  float-to-char float-to-int
                  float-to-long double-to-byte
                  double-to-short double-to-char
                  double-to-int double-to-long
                  double-to-float byte-to-char))