Check that a function to translate to Java does not use any AIJ types.
(atj-check-no-aij-types+body in-types out-types body fn) → yes/no
We check the argument and result types, as well as the body.
Function:
(defun atj-check-no-aij-types+body (in-types out-types body fn) (declare (xargs :guard (and (atj-type-listp in-types) (atj-type-listp out-types) (pseudo-termp body) (symbolp fn)))) (let ((__function__ 'atj-check-no-aij-types+body)) (declare (ignorable __function__)) (and (atj-check-no-aij-type-list in-types fn) (atj-check-no-aij-type-list out-types fn) (atj-check-no-aij-term body fn))))
Theorem:
(defthm booleanp-of-atj-check-no-aij-types+body (b* ((yes/no (atj-check-no-aij-types+body in-types out-types body fn))) (booleanp yes/no)) :rule-classes :rewrite)