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