lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

feat: attributes on {macro,elab}(_rules)

Open digama0 opened this issue 3 years ago • 0 comments

Adds support for attributes on macro, elab, macro_rules, elab_rules. For macro and elab the attributes only apply to the syntax definition, not the macro_rules / elab_rules auxiliary definition along with it.

This PR changes stdlib_flags.h so it requires a stage0 update after merge to reset it.

digama0 avatar Aug 15 '22 00:08 digama0