Recoginizer for smtlink-option-type.
(smtlink-option-type-p option-type) → syntax-good?
Function:
(defun smtlink-option-type-p (option-type) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-option-type-p)) (declare (ignorable acl2::__function__)) (if (member-equal option-type *smtlink-option-types*) t nil)))
Theorem:
(defthm booleanp-of-smtlink-option-type-p (b* ((syntax-good? (smtlink-option-type-p option-type))) (booleanp syntax-good?)) :rule-classes :rewrite)