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?
Comments
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...