### 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 *.