Name of the method to convert a Java expression to a Java primitive array type.
(atj-convert-expr-to-jprimarr-method-name type) → method-name
See atj-convert-expr-to-jprimarr-method.
Function:
(defun atj-convert-expr-to-jprimarr-method-name (type) (declare (xargs :guard (primitive-typep type))) (let ((__function__ 'atj-convert-expr-to-jprimarr-method-name)) (declare (ignorable __function__)) (primitive-type-case type :boolean "convertToBooleanArray" :char "convertToCharArray" :byte "convertToByteArray" :short "convertToShortArray" :int "convertToIntArray" :long "convertToLongArray" :float (prog2$ (raise "Internal error: type ~x0 not supported." type) "irrelevant") :double (prog2$ (raise "Internal error: type ~x0 not supported." type) "irrelevant"))))
Theorem:
(defthm stringp-of-atj-convert-expr-to-jprimarr-method-name (implies (and (primitive-typep type)) (b* ((method-name (atj-convert-expr-to-jprimarr-method-name type))) (stringp method-name))) :rule-classes :rewrite)
Theorem:
(defthm atj-convert-expr-to-jprimarr-method-name-of-primitive-type-fix-type (equal (atj-convert-expr-to-jprimarr-method-name (primitive-type-fix type)) (atj-convert-expr-to-jprimarr-method-name type)))
Theorem:
(defthm atj-convert-expr-to-jprimarr-method-name-primitive-type-equiv-congruence-on-type (implies (primitive-type-equiv type type-equiv) (equal (atj-convert-expr-to-jprimarr-method-name type) (atj-convert-expr-to-jprimarr-method-name type-equiv))) :rule-classes :congruence)