		Search-engine friendly clone of the ACL2 documentation.

atj-jprim-constr-fns

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

We exclude the functions that model the construction of float and double values, because we only have abstract models of those values for now.

Definition: *atj-jprim-constr-fns*

(defconst *atj-jprim-constr-fns*
  '(boolean-value char-value byte-value
                  short-value int-value long-value))