Evaluating types for smtlink option body.
(eval-smtlink-option-type option-type term) → type-correct?
Function:
(defun eval-smtlink-option-type (option-type term) (declare (xargs :guard (smtlink-option-type-p option-type))) (let ((acl2::__function__ 'eval-smtlink-option-type)) (declare (ignorable acl2::__function__)) (case option-type (function-lst-syntax-p (function-lst-syntax-p term)) (hypothesis-lst-syntax-p (hypothesis-lst-syntax-p term)) (hints-syntax-p (hints-syntax-p term)) (symbol-listp (symbol-listp term)) (booleanp (booleanp term)) (stringp (stringp term)) (smt-solver-params-p (smt-solver-params-p term)) (custom-p (booleanp term)) (t (natp term)))))
Theorem:
(defthm booleanp-of-eval-smtlink-option-type (b* ((type-correct? (eval-smtlink-option-type option-type term))) (booleanp type-correct?)) :rule-classes :rewrite)