Major Section: ACL2-BUILT-INS
* is really a macro that expands to calls of the function
binary-*. So for example
(* x y 4 z)represents the same term as
(binary-* x (binary-* y (binary-* 4 z))).
See binary-*.
* is a Common Lisp function. See any Common Lisp documentation
for more information.
