Return the list of all the output type lists in a function's type information.
(atj-function-type-info->outputs info) → out-typess
Function:
(defun atj-function-type-info->outputs (info) (declare (xargs :guard (atj-function-type-info-p info))) (let ((__function__ 'atj-function-type-info->outputs)) (declare (ignorable __function__)) (cons (atj-function-type->outputs (atj-function-type-info->main info)) (atj-function-type-list->outputs (atj-function-type-info->others info)))))
Theorem:
(defthm atj-type-list-listp-of-atj-function-type-info->outputs (b* ((out-typess (atj-function-type-info->outputs info))) (atj-type-list-listp out-typess)) :rule-classes :rewrite)