Theorems generated by atj-main-function-type for all the outputs of a multi-valued ACL2 function.
(atj-main-function-type-output-theorems fn guard formals nresults rev-out-types hints wrld) → events
This is only used when
The output types are reversed (as suggested by the
Function:
(defun atj-main-function-type-output-theorems (fn guard formals nresults rev-out-types hints wrld) (declare (xargs :guard (and (symbolp fn) (pseudo-termp guard) (symbol-listp formals) (natp nresults) (atj-type-listp rev-out-types) (true-listp hints) (plist-worldp wrld)))) (declare (xargs :guard (= nresults (len rev-out-types)))) (let ((__function__ 'atj-main-function-type-output-theorems)) (declare (ignorable __function__)) (if (zp nresults) nil (cons (atj-main-function-type-output-theorem fn guard formals (1- nresults) (car rev-out-types) hints wrld) (atj-main-function-type-output-theorems fn guard formals (1- nresults) (cdr rev-out-types) hints wrld)))))