Name binding in macro?

Stream: lean4

[Siddharth Bhat]

Consider:

syntax "[foomacro|" "foo" str "]" : term

A macro rule that names a binder $foo runs into an error:

macro_rules
| `([foomacro| foo $foo]) => `($foo)
-- ERROR: expected no space before spliced term or string

Renaming the binder to $bar solve the problem:

macro_rules
| `([foomacro| foo $bar]) => `($bar)

I find this counter-intuitive, since I imagined that the strings in the syntax are not "accessible". Clearly, I'm wrong.

• Is this intended behavior?
• If it is intended, What's the use-case for $foo to clash with the string "foo" that is part of the syntax?

$ lean --version
Lean (version 4.0.0-nightly-2022-01-16, commit 189f4bd372d8, Release)

[Alexander Bentkamp]

The issue is already in

syntax "[foomacro|" "foo" str "]" : term

This will make foo a token and foo can then no longer be used for identifiers:

syntax "[foomacro|" "foo" str "]" : term
def foo := 0 -- ERROR: Expected identifier

Try the & sign:

syntax "[foomacro|" &"foo" str "]" : term

This will not make foo a token. Sometimes doing this causes other issues though that I don't fully understand yet...

[Mario Carneiro]

My understanding of the limitation of &"foo" is that it can't be used when an identifier would also be legal in that position. &"foo" and &"bar" can be disambiguated but not &"foo" term and term