Recursion elimination and auxiliary definition

Stream: lean4

[Leni Aniva]

When do the generations of these auxiliary definitions happen in Lean's source code?

For example, if I declare a recursive function, #print gives an equivalent non-recursive form. Sometimes a match expression turns into .match_1, etc.

[Henrik Böving]

This component is known as the equation compiler and for the most part lives in this directory: https://github.com/leanprover/lean4/tree/master/src/Lean/Elab/PreDefinition