Map an ACL2 function that models a Java primitive array write operation to the corresponding Java method name.
(atj-jprimarr-write-to-method-name fn) → method
Function:
(defun atj-jprimarr-write-to-method-name (fn) (declare (xargs :guard (atj-jprimarr-write-fn-p fn))) (let ((__function__ 'atj-jprimarr-write-to-method-name)) (declare (ignorable __function__)) (atj-primarray-write-method-name (case fn (boolean-array-write (primitive-type-boolean)) (char-array-write (primitive-type-char)) (byte-array-write (primitive-type-byte)) (short-array-write (primitive-type-short)) (int-array-write (primitive-type-int)) (long-array-write (primitive-type-long)) (float-array-write (primitive-type-float)) (double-array-write (primitive-type-double)) (t (prog2$ (impossible) ""))))))
Theorem:
(defthm stringp-of-atj-jprimarr-write-to-method-name (b* ((method (atj-jprimarr-write-to-method-name fn))) (stringp method)) :rule-classes :rewrite)