/=
Test inequality of two numbers
(/= x y) is logically equivalent to (not (equal x
y)).
Unlike equal, /= has a guard requiring both of its
arguments to be numbers. Generally, /= is executed more efficiently than
a combination of not and equal.
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
more information.
Function: /=
(defun /= (x y)
(declare (xargs :guard (and (acl2-numberp x)
(acl2-numberp y))))
(not (equal x y)))
