Theorems with varaibles curly braces vs parenthesis

Stream: new members

[Matt Yan]

I noticed in the natural number game some theorem have variables in curly braces {} yet others are in parenthesis (). My experience so far tells me that the arguments in the curly braces should be left out and inferenced automatically yet the ones in the parenthesis have to be explicitly specified. Is that so? And when can you write a theorem with {}?

[Mario Carneiro]

yes that is true

[Mario Carneiro]

You can write a theorem with {} whenever you want, you just literally use {} around that argument in the theorem statement

[Kalle Kytölä]

If you are interested, in #tpil (Section 2.9) you can read more about implicit arguments (with { ... }) versus explicit arguments (with ( ... )).

As Mario said, you can use them whenever you like. The art is to try to choose implicit or explicit arguments in such a way that the theorems become as convenient as possible to use in the future when you build on them.

[Matt Yan]

Mario Carneiro said:

You can write a theorem with {} whenever you want, you just literally use {} around that argument in the theorem statement

Do people bother using parentheses at all then? Isn't implicit argumets better in all cases?