Zulip Chat Archive

Stream: lean4

Topic: Using repeat as identifier


Alex Keizer (Dec 13 2022 at 18:05):

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 (Dec 13 2022 at 18:07):

these are all keywords

Alex Keizer (Dec 13 2022 at 18:10):

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 (Dec 13 2022 at 18:14):

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 (Dec 13 2022 at 19:44):

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 (Dec 13 2022 at 19:49):

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


Last updated: Dec 20 2023 at 11:08 UTC