Major Section: ACL2-BUILT-INS
And
is the macro for conjunctions. And
takes any number of
arguments. And
returns nil
if one of the arguments is nil
,
but otherwise returns the last argument. If there are no arguments,
and
returns t
.
And
is a Common Lisp macro. See any Common Lisp documentation
for more information.