UNARY-_slash_.html -- ACL2 Version 6.2

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