set fty types
(set-fty-types content hint) → new-hint
Function:
(defun set-fty-types (content hint) (declare (xargs :guard (and (symbol-listp content) (smtlink-hint-p hint)))) (let ((acl2::__function__ 'set-fty-types)) (declare (ignorable acl2::__function__)) (b* ((hint (smtlink-hint-fix hint)) (new-hint (change-smtlink-hint hint :fty content))) new-hint)))
Theorem:
(defthm smtlink-hint-p-of-set-fty-types (b* ((new-hint (set-fty-types content hint))) (smtlink-hint-p new-hint)) :rule-classes :rewrite)