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