|
|
|
|
|
|
by fn-mote
29 days ago
|
|
|
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... |
|
|