Arithmetic negation function
Completion Axiom (completion-of-unary-minus):
(equal (unary-- x)
(if (acl2-numberp x)
Guard for (unary-- x):
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 -.