macro nonReservedSymbol?

Stream: lean4

[Sebastian Ullrich]

Not pretty, but fooSym:&"foo"

[Mac]

Sebastian Ullrich said:

Not pretty, but fooSym:&"foo"

Ah, would it be possible for macros to support the underscore for irrelevant values (i.e., _:&"foo")?

[Sebastian Ullrich]

That, or not requiring the ident: part in the first place

[Mac]

That would also be great, but I am not sure if all stx terms can be lifted unambiguously into macro (so _:stx may still be useful in some cases).