Major Section:  ACL2-BUILT-INS

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.

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 ineffecient. 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))


Or is a Common Lisp macro. See any Common Lisp documentation for more information.