Major Section: ACL2-BUILT-INS
Xor is the ACL2 exclusive-or function. (xor P Q) means that either P or Q, but not both, is false (i.e., nil).
Xor
(xor P Q)
P
Q
nil
To see the ACL2 definition of this function, see pf.