Ludicrous bracket suggestion

Stream: general

[Kevin Buzzard]

So I go around schools in the UK giving talks about Lean. In one of these talks I define nat as an inductive type and show schoolkids several ways of proving $2+2=4$.

One thing in Lean which is a bit distracting for people who aren't used to engaging with computers is the boilerplate. For example I might define nat.add and then apologise for instance : has_add nat := \<nat.add\>. Another thing which is a bit distracting for people with a mathematical background is this functional programming trick where you guys write f x instead of $f(x)$, the former being a notation which is not taught at all at schools in the UK. In the past when giving the nat talk I would have to apologise about the lack of brackets, but nowadays I have to apologise about both the lack of brackets and the boilerplate, as I write attribute [pp_nodot] mynat.S to stop Lean unfolding one to zero.S and then it still writes S zero instead of S(zero), even though I'd just spent 2 minutes explanining that S is a function (the successor function).

It just occurred to me that it might be possible for someone (unfortunately not me, unless I'm super-guided by someone!) to write attribute [pp_math_brackets_ftw] mynat.S so that four unfolds to S(three) in the prettyprinter. I cannot imagine anyone in CS using this, but given that right now I have to add a line of boilerplate to switch off dot notation (I can't hide it behind an import because I want to create the inductive type live) so I was wondering whether I could kill these two very minor annoyances with one stone. In talks on other subjects I might just start with "import tactic; open_locale classical" or whatever (at the beginning, where it's Ok to be incomprehensible because I can just make a joke about "switching Lean on" and tell people to ignore it). I guess even open_locale never_dot_notation would be a step in the right direction because then the distracting noise happens before we've got into the meat of the talk.

[Gabriel Ebner]

I guess even open_locale never_dot_notation would be a step [...]

You can do set_option pp.generalized_field_notation false.

[Gabriel Ebner]

Note that S(zero) won't parse in Lean 4 (unless you create your own macro).

[Mario Carneiro]

Is there a conflict for S(zero) in lean 4, or is this just lean 4 being opinionated?

[Gabriel Ebner]

I think we had this in the lean4 channel the other day. No spaces before parens means macro now.

[Mario Carneiro]

yes, but that's just a convention. I can't imagine that it causes much more issue than the occasional name conflict if you have a function called nat_lit or something

[Gabriel Ebner]

Right, it's an unambiguous convention because S(zero) doesn't parse as an application.

[Mario Carneiro]

My question is what would happen if we allowed (or even enforced, as in Kevin's suggestion) writing applications using f(x) style

[Mario Carneiro]

possibly using a syntax extension

[Mario Carneiro]

there aren't that many macros and they have funny names so the conflict there seems not so important

[Gabriel Ebner]

I believe you can add priorities to parsers, so maybe you can add old-school function syntax without breaking macros.

[Kevin Buzzard]

This is interesting, because when I am doing live coding in front of either mathematicians or schoolkids I always put the brackets in (e.g. I define one := S(zero), two := S(one) etc, and hang the prettyprinter because nobody can see it when I'm doing this)

[Sebastien Gouezel]

Am I right that in Lean 4 you'll just need to add a space, i.e., S (zero) instead of S(zero)? This is more readable in any case, so you should already be doing this in Lean 3 :-)

[Kevin Buzzard]

I don't see you putting this space in any of your math papers Sebastien?

[Mario Carneiro]

solution: zero-width space

[Kevin Buzzard]

Another trick I've used is that S(S(S(zero))) is pretty-printed as S (S (S zero))) and if you use enough Ss it's far harder to spot the missing bracket in the middle.

[Sebastien Gouezel]

Kevin Buzzard said:

I don't see you putting this space in any of your math papers Sebastien?

Of course I do in tex sources. Then latex knows what to do here (i.e., ignore whitespace between dollars, but insert a thin space).

[Sebastien Gouezel]

(To be honest, I just checked my last paper, and the first I find is $\liminf d(o, Z_n \cdot o)/n \geq \kappa$, so, without the space :-)

[Oliver Nash]

Using ≥ too, that expression better be inside a quantifier.

[Kevin Buzzard]

yeah, I had forgotten you were allowed to use $\geq$ IRL.