Using repeat as identifier

Stream: lean4

[Alex Keizer]

Lean won't let me add a definition named repeat, try, or calc

def calc := "calc"
def try := "try"
def repeat := "repeat"

Each time failing with expected identifier.

At first I thought there was some conflict with the tactics, but then apply or simp are accepted as identifiers. Is this intended, or some parser bug?

[Mario Carneiro]

these are all keywords

[Alex Keizer]

Ah, thanks. I somehow thought they weren't since VS code doesn't highlight them. Teaches me to rely on highlighting too much ;)

[Mario Carneiro]

they should be highlighted as keywords by the semantic highlighting feature, although possibly that doesn't trigger if there is a parse error

[Alex Keizer]

That's what threw me off; keywords like def and theorem are indeed highlighted when used as identifier, but calc/try/repeat are not.

[Reid Barton]

I believe the syntax highlighting has knowledge of some of the more built-in keywords like def, but in general relies on information from the Lean server