parse Name containing .num

Stream: lean4

[Marcus Rossel]

What's the best way to parse a Name? Lean's ident parser works fine for things like a.b.c, but as soon as a number is involved (as in a.1), it fails.

[Shreyas Srinivas]

There is a name parser. Does it work?

[Marcus Rossel]

No, it doesn't

[Mario Carneiro]

.num components cannot be parsed by the name parser, those are magic internal names that can only be produced with metaprogramming

[Mario Carneiro]

That said I have been thinking about making a raw_name% parser which allows a.1 to be parsed. The trouble is that this would not be an ident so you couldn't just use it anywhere an ident is expected, so you would have to resort to the same macro trick I've used previously, and in that case having a special name parser wouldn't help that much