List of (the names of) the ACL2 functions that model the deconstruction of Java primitive values.
These are the inverses of the functions that model the construction of primitive values. These deconstructors essentially convert the Java primitive values to the corresponding ACL2 values (symbols and integers).
Definition:
(defconst *atj-jprim-deconstr-fns* '(boolean-value->bool$inline char-value->nat$inline byte-value->int$inline short-value->int$inline int-value->int$inline long-value->int$inline))