		Search-engine friendly clone of the ACL2 documentation.

Utilities

Or*

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

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

Definitions and Theorems

Function: binary-or*

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

Function: or*-macro

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