/=

Major Section:  ACL2-BUILT-INS

(/= 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.