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