|
|
|---|
|
|
|
|---|
List of (the names of) the ACL2 functions that model the writing of components of Java primitive arrays.
Definition:
(defconst *atj-jprimarr-write-fns* '(boolean-array-write char-array-write byte-array-write short-array-write int-array-write long-array-write float-array-write double-array-write))