Major Section: ACL2-BUILT-INS
Or is the macro for disjunctions.
Or takes any number of
arguments and returns the first that is non-
there is no non-
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
xwere 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.