Lift atj-process-output-type-spec to lists.
(atj-process-output-type-specs out-type-specs formals in-types) → (mv types arrays)
Function:
(defun atj-process-output-type-specs (out-type-specs formals in-types) (declare (xargs :guard (and (true-listp out-type-specs) (symbol-listp formals) (atj-type-listp in-types)))) (declare (xargs :guard (= (len formals) (len in-types)))) (let ((__function__ 'atj-process-output-type-specs)) (declare (ignorable __function__)) (b* (((when (endp out-type-specs)) (mv nil nil)) ((mv type array) (atj-process-output-type-spec (car out-type-specs) formals in-types)) ((mv types arrays) (atj-process-output-type-specs (cdr out-type-specs) formals in-types))) (mv (cons type types) (cons array arrays)))))
Theorem:
(defthm atj-type-listp-of-atj-process-output-type-specs.types (b* (((mv ?types ?arrays) (atj-process-output-type-specs out-type-specs formals in-types))) (atj-type-listp types)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atj-process-output-type-specs.arrays (b* (((mv ?types ?arrays) (atj-process-output-type-specs out-type-specs formals in-types))) (symbol-listp arrays)) :rule-classes :rewrite)