[nylonstrung]

I'd implore anyone interested in metaprogramming to look at Lean4

It gets overshadowed by the theorem proving but it's unsurpassed in metaprogramming, to my knowledge it can do anything Lisp Racket and Rhombus can and much more

[fn-mote]

I was curious about the meta programming in Lean4 so I poked around a bit. [1] It’s hard to judge a complex system from a quick glance.

I don’t know about power, but the syntax was noisy. (It’s hard to judge how important that is.)

Can anyone comment more? Does the meta-programming stuff get exactly the same checks as regular programming? What kind of error messages do you get from parse failures when your metaprogramming code is being used?

[1]: https://leanprover-community.github.io/lean4-metaprogramming...

[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.