style guide concerning macros that add parens for fn calls

Stream: new members

[Rado Kirov]

I am working with SL from mathlib and SL(2,F) is kinda throwing me off given that we don't use parens and commas for fn calls in Lean. Is this accepted best style to add parens for common math objects? Where does one draw the line?

It's great that Lean is flexible enough to support it, but feels a bit hacky - for example SL (2, F) is syntax error.

Also, not a big deal, just a passing curiosity as I am learning more about Lean.

[Eric Wieser]

I think using parens in macros to distinguish them from regular functions is encouraged

[Damiano Testa]

In this particular case, in informal maths I would write SL₂(F), with optional parentheses around the F.

[Kenny Lau]

@Rado Kirov the observation here is that normal brackets require a space before it, so we're taking advantage of this fact and declaring xx( to be a macro, and this is used in a lot of places (even in core lean). another such widely used macro is congr(.

[Rado Kirov]

In this particular case, in informal maths I would write SL₂(F), with optional parentheses around the F.

But in any informal math you also write φ(x) and σ(x) (say for totient and permutation functions) but adding macros for those to use parens will surely be too much. So SL and GL (and I am not sure what else in mathlib) are somehow special and more "consturctor-y" than "function-y" which justifies the macro? I am thinking about what is the principle for which math functions get parenthesized macros and which shouldn't.

congr(...) and ofNat(...) are more clearly different beasts.