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)) T ACL2>
Or is a Common Lisp macro. See any Common Lisp documentation
for more information.
