Convert a Java expression from a Java primitive array type.
(atj-convert-expr-from-jprimarr expr type) → new-expr
Function:
(defun atj-convert-expr-from-jprimarr (expr type) (declare (xargs :guard (and (jexprp expr) (primitive-typep type)))) (let ((__function__ 'atj-convert-expr-from-jprimarr)) (declare (ignorable __function__)) (b* ((method-name (atj-convert-expr-from-jprimarr-method-name type))) (jexpr-method method-name (list expr)))))
Theorem:
(defthm jexprp-of-atj-convert-expr-from-jprimarr (b* ((new-expr (atj-convert-expr-from-jprimarr expr type))) (jexprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm atj-convert-expr-from-jprimarr-of-jexpr-fix-expr (equal (atj-convert-expr-from-jprimarr (jexpr-fix expr) type) (atj-convert-expr-from-jprimarr expr type)))
Theorem:
(defthm atj-convert-expr-from-jprimarr-jexpr-equiv-congruence-on-expr (implies (jexpr-equiv expr expr-equiv) (equal (atj-convert-expr-from-jprimarr expr type) (atj-convert-expr-from-jprimarr expr-equiv type))) :rule-classes :congruence)
Theorem:
(defthm atj-convert-expr-from-jprimarr-of-primitive-type-fix-type (equal (atj-convert-expr-from-jprimarr expr (primitive-type-fix type)) (atj-convert-expr-from-jprimarr expr type)))
Theorem:
(defthm atj-convert-expr-from-jprimarr-primitive-type-equiv-congruence-on-type (implies (primitive-type-equiv type type-equiv) (equal (atj-convert-expr-from-jprimarr expr type) (atj-convert-expr-from-jprimarr expr type-equiv))) :rule-classes :congruence)