Information about autogenerated definitions

Stream: general

[Vilim Lendvaj]

For stuff like eq1, eq_def, rec, casesOn, noConfusion, etc.
The documentation that I could find is scattered over different language reference pages, and the descriptions are very vague and handwavy. Some don't even have examples.
Is there a comprehensive listing of them, with rigorous formulas to derive their exact type for a given item?