Major Section: ACL2-BUILT-INS
Cond is the construct for IF, THEN, ELSE IF, ... The test is
nil. The argument list for
cond is a list of
``clauses'', each of which is a list. In ACL2, clauses must have
length 1 or 2.
Cond is a Common Lisp macro. See any Common Lisp
documentation for more information.