		Search-engine friendly clone of the ACL2 documentation.

Smtlink-hint-syntax

Smtlink-option-name-fix

Fixing function for smtlink-option-name.

Signature
(smtlink-option-name-fix option) → fixed-smtlink-option-name
Arguments: option — Guard (smtlink-option-name-p option).
Returns: fixed-smtlink-option-name — Type (smtlink-option-name-p fixed-smtlink-option-name).

Definitions and Theorems

Function: smtlink-option-name-fix

(defun smtlink-option-name-fix (option)
  (declare (xargs :guard (smtlink-option-name-p option)))
  (let ((acl2::__function__ 'smtlink-option-name-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (smtlink-option-name-p option)
             option
           ':functions)
         :exec option)))

Theorem: smtlink-option-name-p-of-smtlink-option-name-fix

(defthm smtlink-option-name-p-of-smtlink-option-name-fix
  (b* ((fixed-smtlink-option-name (smtlink-option-name-fix option)))
    (smtlink-option-name-p fixed-smtlink-option-name))
  :rule-classes :rewrite)