+

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