Reference for equations compiler using brecOn

Stream: lean4

[Yannick Forster]

My understanding is that any recursive function definition in Lean is compiled to an application of the brecOn combinator of the inductive type the recursion works on, and brecOn is defined automatically using rec at definition time of the inductive type. The equations compiler even uses brecOn for functions which could be defined with rec directly. Is there a reference for this behaviour? It's not mentioned in the CADE '21 paper I think. It's kind of there in https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/, but still a bit implicit (@Joachim Breitner)

[Joachim Breitner]

That's all correct (well, there are also partial recursive functions and those using well-founded recursion). I don't know of any reference for the lean implementation though. Eventually we'll have a reference manual.