		Search-engine friendly clone of the ACL2 documentation.

Smtlink-hint-syntax

Smtlink-hint-syntax-fix

Fixing function for smtlink-hint-syntax.

Signature
(smtlink-hint-syntax-fix term) → fixed-smtlink-hint-syntax
Arguments: term — Guard (smtlink-hint-syntax-p term).
Returns: fixed-smtlink-hint-syntax — Type (smtlink-hint-syntax-p fixed-smtlink-hint-syntax).

Definitions and Theorems

Function: smtlink-hint-syntax-fix

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

Theorem: smtlink-hint-syntax-p-of-smtlink-hint-syntax-fix

(defthm smtlink-hint-syntax-p-of-smtlink-hint-syntax-fix
  (b* ((fixed-smtlink-hint-syntax (smtlink-hint-syntax-fix term)))
    (smtlink-hint-syntax-p fixed-smtlink-hint-syntax))
  :rule-classes :rewrite)

Theorem: smtlink-hint-syntax-fix-when-smtlink-hint-syntax-p

(defthm smtlink-hint-syntax-fix-when-smtlink-hint-syntax-p
  (b* ((fixed-smtlink-hint-syntax (smtlink-hint-syntax-fix term)))
    (implies (smtlink-hint-syntax-p term)
             (equal fixed-smtlink-hint-syntax term)))
  :rule-classes :rewrite)