Test equality of two numbers
(= x y) is logically equivalent to (equal x y).
Unlike equal, = has a guard requiring both of its
arguments to be numbers. Generally, = is executed more efficiently than
For a discussion of the various ways to test against 0, See zero-test-idioms.
= is a Common Lisp function. See any Common Lisp documentation for
(defun = (x y)
(declare (xargs :guard (and (acl2-numberp x)
(equal x y))