UNARY--.html -- ACL2 Version 3.1

UNARY--

arithmetic negation function

Major Section:  PROGRAMMING

Completion Axiom:

(equal (unary-- x)
       (if (acl2-numberp x)
           (unary-- x)
         0))

Guard for (unary-- x):

(acl2-numberp 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 -.