		Search-engine friendly clone of the ACL2 documentation.

Hypothesis-lst-syntax

Hypothesis-lst-syntax-fix

Fixing function for a hypothesis-lst-syntax-p.

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

Definitions and Theorems

Function: hypothesis-lst-syntax-fix

(defun hypothesis-lst-syntax-fix (term)
  (declare (xargs :guard (hypothesis-lst-syntax-p term)))
  (let ((acl2::__function__ 'hypothesis-lst-syntax-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (consp term)
             (cons (hypothesis-syntax-fix (car term))
                   (hypothesis-lst-syntax-fix (cdr term)))
           nil)
         :exec term)))

Theorem: hypothesis-lst-syntax-p-of-hypothesis-lst-syntax-fix

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