		Search-engine friendly clone of the ACL2 documentation.

Function-syntax

Function-option-lst-syntax-fix

Recogizer for function-option-lst-syntax

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

Definitions and Theorems

Function: function-option-lst-syntax-fix

(defun function-option-lst-syntax-fix (term)
  (declare (xargs :guard (function-option-lst-syntax-p term)))
  (let ((acl2::__function__ 'function-option-lst-syntax-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (function-option-lst-syntax-p term)
             term
           nil)
         :exec term)))

Theorem: function-option-lst-syntax-p-of-function-option-lst-syntax-fix

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

Theorem: function-option-lst-syntax-fix-when-function-option-lst-syntaxp

(defthm
    function-option-lst-syntax-fix-when-function-option-lst-syntaxp
  (b* ((fixed-term (function-option-lst-syntax-fix term)))
    (implies (function-option-lst-syntax-p term)
             (equal fixed-term term)))
  :rule-classes :rewrite)