if-then-else function
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.