Evaluating types for function option body.
(eval-function-option-type option-type term) → type-correct?
Function:
(defun eval-function-option-type (option-type term) (declare (xargs :guard (function-option-type-p option-type))) (let ((acl2::__function__ 'eval-function-option-type)) (declare (ignorable acl2::__function__)) (b* ((option-type (function-option-type-fix option-type))) (case option-type (argument-lst-syntax-p (argument-lst-syntax-p term)) (natp (natp term)) (hypothesis-syntax-p (hypothesis-syntax-p term)) (t (hypothesis-lst-syntax-p term))))))
Theorem:
(defthm booleanp-of-eval-function-option-type (b* ((type-correct? (eval-function-option-type option-type term))) (booleanp type-correct?)) :rule-classes :rewrite)