		Search-engine friendly clone of the ACL2 documentation.

Binary-+

Addition function

Completion Axiom (completion-of-+):

(equal (binary-+ x y)
       (if (acl2-numberp x)
           (if (acl2-numberp y)
               (binary-+ x y)
             x)
         (if (acl2-numberp y)
             y
           0)))

Guard for (binary-+ x y):

(and (acl2-numberp x) (acl2-numberp y))

Notice that like all arithmetic functions, binary-+ treats non-numeric inputs as 0. Thus, the following are theorems.

(thm (equal (+ (fix x) y) (+ x y)))
(thm (equal (+ x (fix y)) (+ x y)))

Calls of the macro + expand to calls of binary-+; see +.