Theorem generated by atj-main-function-type for an input of an ACL2 function.
(atj-main-function-type-input-theorem fn guard formal in-type hints wrld) → event
The theorem states that, under the guard, the specified formal argument satisfies the predicate that corresponds to the specified type.
The theorem has no rule classes because its only purpose is to make sure that its formula holds. The theorem is local (to the encapsulate generated by the macro) for the same reason.
Function:
(defun atj-main-function-type-input-theorem (fn guard formal in-type hints wrld) (declare (xargs :guard (and (symbolp fn) (pseudo-termp guard) (symbolp formal) (atj-typep in-type) (true-listp hints) (plist-worldp wrld)))) (let ((__function__ 'atj-main-function-type-input-theorem)) (declare (ignorable __function__)) (b* ((thm-name (packn-pos (list 'atj- fn '-input- formal '- (atj-type-to-keyword in-type)) (pkg-witness (symbol-package-name fn)))) (thm-formula (implicate guard (cons (atj-type-to-pred in-type) (cons formal 'nil))))) (cons 'local (cons (cons 'defthm (cons thm-name (cons (untranslate thm-formula t wrld) (cons ':rule-classes (cons 'nil (cons ':hints (cons hints 'nil))))))) 'nil)))))