+

addition macro
Major Section:  ACL2-BUILT-INS

+ is really a macro that expands to calls of the function binary-+. So for example

(+ x y 4 z)
represents the same term as
(binary-+ x (binary-+ y (binary-+ 4 z))).
See binary-+.