Theorems generated by atj-main-function-type for all the inputs of an ACL2 function.
(atj-main-function-type-input-theorems fn guard formals in-types hints wrld) → events
This lifts atj-main-function-type-input-theorem to lists.
Function:
(defun atj-main-function-type-input-theorems (fn guard formals in-types hints wrld) (declare (xargs :guard (and (symbolp fn) (pseudo-termp guard) (symbol-listp formals) (atj-type-listp in-types) (true-listp hints) (plist-worldp wrld)))) (declare (xargs :guard (= (len formals) (len in-types)))) (let ((__function__ 'atj-main-function-type-input-theorems)) (declare (ignorable __function__)) (if (endp formals) nil (cons (atj-main-function-type-input-theorem fn guard (car formals) (car in-types) hints wrld) (atj-main-function-type-input-theorems fn guard (cdr formals) (cdr in-types) hints wrld)))))