Major Section: ACL2-BUILT-INS
See binary-* for multiplication and see unary-/ for reciprocal.
/ 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
/is a Common Lisp macro. See any Common Lisp documentation for more information.