Set :int-to-rat based on user hint.
(set-int-to-rat content hint) → new-hint
Function:
(defun set-int-to-rat (content hint) (declare (xargs :guard (and (booleanp content) (smtlink-hint-p hint)))) (let ((acl2::__function__ 'set-int-to-rat)) (declare (ignorable acl2::__function__)) (b* ((hint (smtlink-hint-fix hint)) (new-hint (change-smtlink-hint hint :int-to-rat content))) new-hint)))
Theorem:
(defthm smtlink-hint-p-of-set-int-to-rat (b* ((new-hint (set-int-to-rat content hint))) (smtlink-hint-p new-hint)) :rule-classes :rewrite)