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