FYI: 'An Extensible Theorem Proving Frontend' by S. Ullrich

Stream: lean4

[Yuri de Wit]

I just realized a new PDF by Sebastian Ullrich (dissertation) has been linked to Lean's website with a wealth of information on Lean's extensible frontend.

I believe others will find it interesting too: https://leanprover.github.io/papers/thesis-sebastian.pdf