Fixing function for smtlink-option-type.
(smtlink-option-type-fix opttype) → fixed-opttype
Function:
(defun smtlink-option-type-fix (opttype) (declare (xargs :guard (smtlink-option-type-p opttype))) (let ((acl2::__function__ 'smtlink-option-type-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (smtlink-option-type-p opttype) opttype 'function-lst-syntax-p) :exec opttype)))
Theorem:
(defthm smtlink-option-type-p-of-smtlink-option-type-fix (b* ((fixed-opttype (smtlink-option-type-fix opttype))) (smtlink-option-type-p fixed-opttype)) :rule-classes :rewrite)