BINARY-+

addition function 
Major Section:  ACL2-BUILT-INS

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.

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