Major Section: PROGRAMMING

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

(iff P Q)

P

Q

nil