Preventing attribute syntax from stealing identifiers

Stream: lean4

[Jannis Limperg]

I'm working on a tactic that will require a somewhat complicated attribute grammar. E.g. something like

@[aesop (builder tactic) (priority 50) safe]`

Lean 4 allows me to cleanly define this syntax using syntax declarations (which is awesome), but then builder, tactic, priority, safe etc. become reserved words. Can I somehow tell the parser to treat them as keywords only in attributes? I guess the usual answer to questions like this is scoping, but that would be cumbersome here.

[Sebastian Ullrich]

You can match against literal identifiers without making them keywords: https://github.com/leanprover/lean4/blob/master/tests/lean/nonReserved.lean

[Gabriel Ebner]

Is there some kind of cheatsheet for the various syntax notations?

[Gabriel Ebner]

This is the first time I've seen this &. I wonder how much else I've been missing out on.

[Sebastian Ullrich]

Not that I know of, but they should be at either https://github.com/leanprover/lean4/blob/e68d09704d3a6494974de8b921d5b1b5cd1473df/src/Init/Notation.lean#L41-L61 or https://github.com/leanprover/lean4/blob/e68d09704d3a6494974de8b921d5b1b5cd1473df/src/Lean/Parser/Syntax.lean#L32-L39. A nice table summarizing them sounds like a great contribution to the manual :) .

[Jannis Limperg]

Nice! That's exactly what I was hoping for.

[Sebastian Ullrich]

The underlying initial parser encoding is at https://github.com/leanprover/lean4/blob/e68d09704d3a6494974de8b921d5b1b5cd1473df/src/Init/Prelude.lean#L1848-L1860. The available Names in there are more scattered though, via registerAlias/register_parser_alias calls