Or
Disjunction
Or is the macro for disjunctions. Or takes any number of
arguments and returns the first that is non-nil, or nil if there is
no non-nil element.
(Note: If you are seeking documentation for the :or hint, see hints.)
In the ACL2 logic, the macroexpansion of (or x y) is an IF term
that appears to cause x to be evaluated twice:
ACL2 !>:trans (or x y)
(IF X X Y)
=> *
ACL2 !>
If x were replaced by an expression whose evaluation takes a long
time, then such an expansion would be inefficient. However, don't be fooled:
you can expect Common Lisp implementations to avoid this problem, say by
generating a new variable, for example:
ACL2 !>:q ; Exit the ACL2 loop and go into raw Common Lisp
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(macroexpand '(or x y))
(LET ((#:G5374 X)) (IF #:G5374 #:G5374 Y))
T
ACL2>
Or is a Common Lisp macro. See any Common Lisp documentation for more
information.
Macro: or
(defmacro or (&rest args)
(or-macro args))
Function: or-macro
(defun or-macro (lst)
(declare (xargs :guard t))
(if (consp lst)
(if (consp (cdr lst))
(list 'if
(car lst)
(car lst)
(or-macro (cdr lst)))
(car lst))
nil))
