Comment by jonny_eh

Apparently this is possible with macros? I dunno: https://github.com/leanprover/lean3/issues/1355