Fixing function for function-option-type.
(function-option-type-fix option-type) → fixed-option-type
Function:
(defun function-option-type-fix (option-type) (declare (xargs :guard (function-option-type-p option-type))) (let ((acl2::__function__ 'function-option-type-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (function-option-type-p option-type) option-type 'natp) :exec option-type)))
Theorem:
(defthm function-option-type-p-of-function-option-type-fix (b* ((fixed-option-type (function-option-type-fix option-type))) (function-option-type-p fixed-option-type)) :rule-classes :rewrite)