behavior of keywords and syntax cat declaration

Stream: lean4

[Remy Citerin]

Hi! I recently put an issue on lean4 (https://github.com/leanprover/lean4/issues/2308), but I'm not convinced by the answer, here's my reasoning:

In my case foo is a syntactic category independent of term, ident and all the other categories used in the construction of the structure (it's also work if I replace syntax " bar " term : foo by syntax " bar " foo : foo), so I don't understand why it would be desirable for the default behavior to break this independence.

Is there a reason for this design (performance issue, etc.)?

[Mario Carneiro]

It's not desirable, but it is the current situation

[Mario Carneiro]

There are discussions about how to lift this restriction (context-dependent token maps) and I think an open PR lean4#2293 that relates to it