From time to time I'm starting a Theorem prover tutorial, sometimes I even finish. The learning curve is long.

Thanks, I looked at the Agda version. It is more explicit and well documented.

And I agree: tactics are another thing to learn and can be very arcane.

But in this discussion everybody admires Isabelle/Hol's automation: "I'm envious of the degree of automation that Isabelle affords".

---

My problem with "theorem eval_eval : x ~>* (eval x).embed" was very basic.

I got confused by the infix definition of "~>*".

Viewing the type in the playground as "∀ {a : Ty} {x : Exp a}, RTC Eval x (Val.embed a (eval x))" helped.

---

I am just dabbling around but I will try Lean 4. It seems to work well though it is not officially released.

And Lean 4 seems to be a very fast funcional programming language.

(I actually finished an Agda Tutorial a few years ago, it's focus is on programming. Lean somehow succeeded to "fix" or "hack around" this annoying intensional equality:

"Lean's standard library defines an additional axiom, propositional extensionality, and a quotient construction which in turn implies the principle of function extensionality"

)