### UNARY-/

reciprocal function
Major Section: ACL2-BUILT-INS

Completion Axiom (`completion-of-unary-/`

):

(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 /.