|
|
|---|
|
|
|
|---|
List of (the names of) the ACL2 functions that model Java primitive array operations.
Definition:
(defconst *atj-jprimarr-fns* (append *atj-jprimarr-read-fns* *atj-jprimarr-length-fns* *atj-jprimarr-write-fns* *atj-jprimarr-new-len-fns* *atj-jprimarr-new-init-fns* *atj-jprimarr-conv-tolist-fns* *atj-jprimarr-conv-fromlist-fns*))