		Search-engine friendly clone of the ACL2 documentation.

Function-option-name-list

Function-option-name-fix

Fixing function for option.

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

Definitions and Theorems

Function: function-option-name-fix

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

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

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