custom error message for syntax category expectation

Stream: lean4

[Thomas Murrills]

If I have a syntax category

declare_syntax_cat foo
syntax "a" <|> "b" : foo -- or some other syntax, details unimportant

declare_syntax_cat bar
syntax "bar! " foo : tactic

then when I type bar! c in a tactic, I'll see "expected foo" as an error message.

I'd like to manually change this error message for foo so that it's more descriptive—e.g. "expected 'a' or 'b'". Is there a way to do that?

[Sebastian Ullrich]

That would seem to contradict the extensibility of syntax categories. Use syntax foo := "a" <|> "b" if you don't need that.