[gopiandcode]

Oh, really? I'm curious what exactly you mean by limitless metaprogramming. I've really been drawn into Lean specifically because of how easy to extend and malleable the language itself is, so if Agda is even more so then I'd be really eager to try that out.

e.g.:

- embedding a prolog/asp DSL: https://github.com/kiranandcode/cleango

- embedding a tex/latex DSL: https://github.com/kiranandcode/LeanTeX

[yuppiemephisto]

I was surprised to hear their claim about Agda's metaprogramming, I say lean is better here