Major Section: ACL2-BUILT-INS
See binary-* for multiplication and see unary-/ for reciprocal.
Note that / represents division as follows:
(/ x y)represents the same term as
(* x (/ y))which is really
(binary-* x (unary-/ y)).Also note that
/ represents reciprocal as follows:
(/ x)expands to
(unary-/ x).
/ is a Common Lisp macro. See any Common Lisp documentation
for more information.
