BINARY-*

multiplication 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)
             0)
         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 *.