Major Section: ACL2-BUILT-INS
Completion Axiom (
(equal (unary-/ x) (if (and (acl2-numberp x) (not (equal x 0))) (unary-/ x) 0))
(and (acl2-numberp x) (not (equal x 0)))Notice that like all arithmetic functions,
unary-/treats non-numeric inputs as
Calls of the macro
/ on one argument expand to calls of
unary-/; see /.