BINARY-+

addition function

Major Section: PROGRAMMING

Completion Axiom:

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