Major Section: ACL2-BUILT-INS
(if x y z) is equal to y if x is any value
other than nil, and is equal to z if x is nil.
Only one of y, z is evaluated when (if x y z) is
evaluated.
If has a guard of t.
If is part of Common Lisp. See any Common Lisp documentation for
more information.
