		Search-engine friendly clone of the ACL2 documentation.

Fgl-syntactic-checker-binders

Check-equal

FGL binder that checks whether X and Y are syntactically equal.

Signature
(check-equal ans x y) → *

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

Definitions and Theorems

Function: check-equal

(defun check-equal (ans x y)
  (declare (xargs :guard t))
  (let ((__function__ 'check-equal))
    (declare (ignorable __function__))
    (and (equal x y) ans t)))

Theorem: check-equal-implies-equal

(defthm check-equal-implies-equal
  (implies (check-equal ans x y)
           (equal x y))
  :rule-classes :forward-chaining)