[mlechu]

I don't think this is true. Lean has hygienic macros, but doesn't appear to have local macros like Racket does; the thing called "local macro" restricts a macro's use to a certain region, but the macro definition can't capture local variables from outside of it.