UNARY--.html -- ACL2 Version 6.1

arithmetic negation function

Major Section:  ACL2-BUILT-INS

Completion Axiom (completion-of-unary-minus):

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