Only allowing certain numerals

Stream: lean4

[Henrik Böving]

Is there a way for me to only allow certain numerals in a custom syntax category, e.g. this:

declare_syntax_cat expr
syntax "0" : expr

gives me a "invalid atom" (which I think is definitley an error message we should improve if possible). Can I do anything about this at the syntax level or do I have to just allow num and check if the numeral is to my liking in the macro / elaborator

[Sebastian Ullrich]

Currently you can't, this would likely be solved with the move to custom and category-local token parsers