		Search-engine friendly clone of the ACL2 documentation.

Utilities

And*

and* is like and but is a (typically disabled) function.

This is occasionally useful for avoiding case-splitting in theorems.

Definitions and Theorems

Function: binary-and*

(defun binary-and* (x y)
  (declare (xargs :guard t))
  (if x y nil))

Function: and*-macro

(defun and*-macro (x)
  (declare (xargs :guard t))
  (cond ((atom x) t)
        ((atom (cdr x)) (car x))
        (t (cons 'binary-and*
                 (cons (car x)
                       (cons (and*-macro (cdr x)) 'nil))))))