		Search-engine friendly clone of the ACL2 documentation.

Fgl-syntactic-checker-binders

Check-int-endp

FGL binder that checks whether X is syntactically a int-endp, i.e. either 0, -1, or not an integer.

Signature
(check-int-endp ans x) → *
Arguments: x — Guard (integerp x).

See fgl-syntactic-checker-binders and see binder for details.

Definitions and Theorems

Function: check-int-endp

(defun check-int-endp (ans x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'check-int-endp))
    (declare (ignorable __function__))
    (and (int-endp x) ans t)))

Theorem: check-int-endp-fn-implies-int-endp

(defthm check-int-endp-fn-implies-int-endp
 (implies
  (acl2::rewriting-negative-literal (cons 'check-int-endp
                                          (cons ans (cons x 'nil))))
  (iff (check-int-endp ans x)
       (and (int-endp x)
            (hide (check-int-endp ans x))))))