Iff
Logical ``if and only if''
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).
Function: iff
(defun iff (p q)
(declare (xargs :guard t))
(if p (if q t nil) (if q nil t)))
