The line between term elaboration and macro

Stream: lean4

[Henrik Böving]

In the meta programming tutorial thread @Jannis Limperg and @Siddhartha Gadgil mentioned that they are rather opposed to macros that are "too powerful", in particular ones that "use Syntax for logic and control" and that they prefer term elaboration / meta code over such macros.

I'm wondering where people think the border between "use a macro" and "use an elaborator" for this actually is. In my mind this has so far been that as soon as types or control flow is involved a macro is probably not reasonable anymore. However based on this I find it rather hard to find examples of things you might want to write as term elaborators that are actually simple (i.e. reasonable as a sort of beginner example for "use a term elab and not a macro for this") because this is precisely what macros seem to be for in my mind, the simple stuff.

[Jannis Limperg]

Don't think there's a hard line (and obviously Sebastian and Leo are not opposed to using macros for significant control flow, so don't take my opinion as gospel on this). For tutorial purposes, I think it's fine to say "this could be done with a macro but we'll do it as an elab for exercise; see later for more realistic examples."