Lift atj-type-conv-allowed-p to lists of types.
(atj-types-conv-allowed-p src-types dst-types) → yes/no
The two lists should always have the same length. The conversion between type lists is allowed if and only if it is allowed element-wise.
Function:
(defun atj-types-conv-allowed-p-aux (src-types dst-types) (declare (xargs :guard (and (atj-type-listp src-types) (atj-type-listp dst-types)))) (declare (xargs :guard (= (len src-types) (len dst-types)))) (let ((__function__ 'atj-types-conv-allowed-p-aux)) (declare (ignorable __function__)) (or (endp src-types) (and (atj-type-conv-allowed-p (car src-types) (car dst-types)) (atj-types-conv-allowed-p-aux (cdr src-types) (cdr dst-types))))))
Theorem:
(defthm booleanp-of-atj-types-conv-allowed-p-aux (b* ((yes/no (atj-types-conv-allowed-p-aux src-types dst-types))) (booleanp yes/no)) :rule-classes :rewrite)
Function:
(defun atj-types-conv-allowed-p (src-types dst-types) (declare (xargs :guard (and (atj-type-listp src-types) (atj-type-listp dst-types)))) (declare (xargs :guard (and (consp src-types) (consp dst-types)))) (let ((__function__ 'atj-types-conv-allowed-p)) (declare (ignorable __function__)) (if (= (len src-types) (len dst-types)) (atj-types-conv-allowed-p-aux src-types dst-types) (raise "Internal error: ~ the type lists ~x0 and ~x1 differe in length." src-types dst-types))))
Theorem:
(defthm booleanp-of-atj-types-conv-allowed-p (b* ((yes/no (atj-types-conv-allowed-p src-types dst-types))) (booleanp yes/no)) :rule-classes :rewrite)