theorems in NNG

Stream: new members

[Lu-Ming Zhang]

image.png
It's in the NNG.
What will be the change of the theorem if I change "{a b : mynat}" in add_right_eq_zero to "(a b : mynat)"?
Another question is that I can't understand the definition of add_left_eq_zero, especially the use of the double brackets {{}}. Could anyone give me an explanation?

[Eric Rodriguez]

these are different ways of taking arguments; (a b : mynat) means your arguments have to be explicit, whilst {a b : mynat} means Lean will try to figure them out for you. The double brackets are slightly different to the single brackets, but not meaningfully so