LOGEQV

bitwise logical equivalence of zero or more integers
Major Section:  ACL2-BUILT-INS

When integers are viewed in their two's complement representation, logeqv returns their bitwise logical equivalence. In ACL2 logeqv is a macro that expands into calls of the binary function binary-logeqv, except that (logeqv) expands to -1 and (logeqv x) expands to x.

The guard for binary-logeqv requires its arguments to be integers. Logeqv is defined in Common Lisp. See any Common Lisp documentation for more information.