RFC: Extensible pre-definition-compilers

Stream: lean4 dev

[Joachim Breitner]

I have been thinking about the various ways recursive definitions can be handled, and comparing with Isabelle, we have to do some catching up. It might be much easier to catch up and unlock interesting applications if the recursive definition processing can be extended just like other parts of elaboration, so I wrote my first Lean RFC: https://github.com/leanprover/lean4/issues/2812
Looking forward to feedback (in particular naming that concept…)