I enjoyed this, hadn't used backpack and this is a nice tutorial

That’s what I was thinking seeing the username =)

Lean 4 truly lets you mathematically reason about code and has metaprogramming that truly makes syntax a surface thing, but if anything people who know this have the taste to want better syntax

We sung it at solstice

`show_term grind` and `by grind?` should do what you want

What do you think of embedding it in a formal system like Lean as a frontend?

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

I don’t know about their motivation, but I would say mine is that Lean is a real programming language. Coq is not really meant for “prosaic” programming, more’s the pity.

Lean is also a lot faster.

No specific motivation tbh. I did the number theory game on the recommendation of a friend and found it fun. Made me think.

What does the real programming language part help in? Developing tactics? Or is it because even when you are typing the "math parts" it corresponds to a real programming language giving you a nicer mental model?

Because from what I understand Rocq too has Gallina or something right?

I guess my other point is Rocq seems to have a lot of textbooks too so I was wondering which one to read about when I get some more time - Rocq or Lean.

>Lean is also a lot faster.

What do you base that on? I don't think I've seen a performance comparison but I'm not great at internet searches.

Maybe too far afield, but: https://leanprover-community.github.io/lean4-metaprogramming...

Gives what you wished for. It's functional, though (among other things). Unlike most lisps, (dependently) typed. But hey, available at compile-time.

> I’d rather have the language …

check out Lean 4 then. Its syntax system is based on Racket but —instead of parens— implements stuff like [JSX syntax](https://github.com/leanprover-community/ProofWidgets4/blob/d...) and a [maze](https://github.com/dwrensha/lean4-maze)