*

multiplication macro
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.