Parentheses for arguments

Stream: new members

[Zihao Zhang]

a b:R,why add_comm (-a) b is right,add _comm -a b is wrong?

[Notification Bot]

A message was moved here from #new members > Using lean as a general language by Ruben Van de Velde.

[Edward van de Meent]

because add_comm -a b means (((fun x y => x - y) add_comm) (a b)) due to the binding priorities of - and function apprlication.

[Eric Wieser]

Or less confusingly, add _comm -a b means (add_comm) - (a b)

[Edward van de Meent]

thanks, i had a hard time phrasing that :+1: