Major Section: ACL2-BUILT-INS
Iff is the ACL2 biconditional, ``if and only if''. (iff P Q)
means that either P and Q are both false (i.e., nil) or both true
(i.e., not nil).
(iff P Q)
To see the ACL2 definition of this function, see pf.